ยซ Up

tactician-api 15.0+8.11 Black list ๐Ÿดโ€โ˜ ๏ธ

Context

# Packages matching: installed
# Name                # Installed # Synopsis
base-bigarray         base
base-threads          base
base-unix             base
conf-gmp              4           Virtual package relying on a GMP lib system installation
coq                   8.18.0      The Coq Proof Assistant
coq-core              8.18.0      The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib            8.18.0      The Coq Proof Assistant -- Standard Library
coqide-server         8.18.0      The Coq Proof Assistant, XML protocol server
dune                  3.13.0      Fast, portable, and opinionated build system
ocaml                 4.14.0      The OCaml compiler (virtual package)
ocaml-base-compiler   4.14.0      Official release 4.14.0
ocaml-config          2           OCaml Switch Configuration
ocaml-options-vanilla 1           Ensure that OCaml is compiled with no special options enabled
ocamlfind             1.9.6       A library manager for OCaml
zarith                1.13        Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
synopsis: "An API exposing Coq's web of formal knowledge to external agents"
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 <lasse@blaauwbroek.eu>"]
authors: ["Lasse Blaauwbroek <lasse@blaauwbroek.eu>"]
license: "MIT"
homepage: "https://coq-tactician.github.io"
bug-reports: "https://github.com/coq-tactician/coq-tactician-api/issues"
build: [
  ["dune" "subst"] {dev}
  [
    "dune"
    "build"
    "-p"
    name
    "-j"
    jobs
    "--promote-install-files=false"
    "@install"
    "@runtest" {with-test}
    "@doc" {with-doc}
  ]
  ["dune" "install" "-p" name "--create-install-files" name]
]
dev-repo: "git+https://github.com/coq-tactician/coq-tactician-api.git"
depends: [
  "ocamlfind"
  "coq" {>= "8.11" & < "8.12~"}
  "coq-tactician" {= "1.0~beta2~neural+8.11"}
  "logs"
  "fmt"
  "capnp-rpc-unix"
  "capnp-rpc-lwt"
  "capnp" {>= "3.4.0"}
  "ppx_deriving"
  "ocamlgraph"
  "xxhash"
  "dune" {>= "2.9"}
  "odoc" {with-doc}
  # These constraints are to work around
  # https://github.com/ocsigen/lwt/issues/764 and
  # https://github.com/ocaml/ocaml/pull/9914
  "ocaml" {>= "4.12~"} | ("ocaml" {< "4.12~"} & "lwt" {<= "5.1.1"})
]
substs: [
  "src/graph_generator_learner.ml"
  "theories/injection-flags-loader"
]
url {
  src: "https://github.com/coq-tactician/coq-tactician-api/archive/refs/tags/v15.0-8.11.tar.gz"
  checksum: "sha512=a42d446726f4cb7a54213f7b546c86165eb3f3901890ad198661424798a4ec676fe22b2e8091683a025da9be834519d73bc518cd405ce0b5fe5c1af47bdea19a"
}

Lint

Command
true
Return code
0

Dry install ๐Ÿœ๏ธ

Dry install with the current Coq version:

Command
opam install -y --show-action coq-tactician-api.15.0+8.11 coq.8.18.0
Return code
5120
Output
[NOTE] Package coq is already installed (current version is 8.18.0).
The following dependencies couldn't be met:
  - coq-tactician-api -> coq < 8.12~ -> ocaml < 4.12
      base of this switch (use `--unlock-base' to force)
No solution found, exiting

Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:

Command
opam remove -y coq; opam install -y --show-action --unlock-base coq-tactician-api.15.0+8.11
Return code
15360
Output
The following actions will be performed:
  - remove coq 8.18.0
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> removed   coq.8.18.0
Done.
# Run eval $(opam env) to update the current shell environment
[ERROR] Sorry, resolution of the request timed out.
        Try to specify a simpler request, use a different solver, or increase the allowed time by setting OPAMSOLVERTIMEOUT to a bigger value (currently, it is set to 600.0 seconds).

Install dependencies

Command
true
Return code
0
Duration
0 s

Install ๐Ÿš€

Command
true
Return code
0
Duration
0 s

Installation size

No files were installed.

Uninstall ๐Ÿงน

Command
true
Return code
0
Missing removes
none
Wrong removes
none