Add opam description

coq-tactician-api.opam

@@ -1,7 +1,14 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
 synopsis: "An API exposing Coq's web of formal knowledge to external agents"
-description: ""
+description: """
+Tactician's API provides external machine learning agents with the data
+   collected by Tactician from the Coq Proof Assistant. It is able to extract
+   large-scale datasets from a wide variety of Coq packages for the purpose of
+   offline machine learning. Additionally, it allows agents to interact with
+   Coq. Proving servers can be connected to Tactician's `synth` tactic and prove
+   theorems for Coq users. Additionally, servers can do proof exploration
+   through the `Tactician Explore` command."""
 maintainer: ["Lasse Blaauwbroek <[email protected]>"]
 authors: ["Lasse Blaauwbroek <[email protected]>"]
 homepage: "https://coq-tactician.github.io"

dune-project

@@ -12,4 +12,11 @@
 (package
  (name coq-tactician-api)
  (synopsis "An API exposing Coq's web of formal knowledge to external agents")
- (description ""))
+ (description
+   "Tactician's API provides external machine learning agents with the data
+   collected by Tactician from the Coq Proof Assistant. It is able to extract
+   large-scale datasets from a wide variety of Coq packages for the purpose of
+   offline machine learning. Additionally, it allows agents to interact with
+   Coq. Proving servers can be connected to Tactician's `synth` tactic and prove
+   theorems for Coq users. Additionally, servers can do proof exploration
+   through the `Tactician Explore` command."))