# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-domains base base-nnp base Naked pointers prohibited in the OCaml heap base-threads base base-unix base conf-gmp 4 Virtual package relying on a GMP lib system installation coq dev The Coq Proof Assistant coq-core dev The Coq Proof Assistant -- Core Binaries and Tools coq-stdlib dev The Coq Proof Assistant -- Standard Library coqide-server dev The Coq Proof Assistant, XML protocol server dune 3.12.2 Fast, portable, and opinionated build system ocaml 5.0.0 The OCaml compiler (virtual package) ocaml-base-compiler 5.0.0 Official release 5.0.0 ocaml-config 3 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" name: "coq-tactician-stdlib" synopsis: "Recompiles Coq's standard libary with Tactician's instrumentation loaded" description: """ *** WARNING *** This package will overwrite Coq's standard library files. This package recompiles Coq's standard library with Tactician's (`coq-tactician`) instrumentation loaded such that Tactician can learn from the library. When you install this package, the current `.vo` files of the standard library are backed in the folder `user-contrib/Tactician/stdlib-backup`. The new `.vo` files are equivalent to the originals, except that they also contain Tactician's tactic databases. After installation of this package, all other Coq developments that are installed will also need to be recompiled. The 'tactician recompile' command line utility can help with this. Upon removal of this package, the original files will be placed back. """ homepage: "https://coq-tactician.github.io" dev-repo: "git+https://github.com/coq-tactician/coq-tactician-stdlib" bug-reports: "https://github.com/coq-tactician/coq-tactician-stdlib/issues" license: "LGPL-2.1-only" maintainer: "Lasse Blaauwbroek <lasse@blaauwbroek.eu>" authors: "Lasse Blaauwbroek <lasse@blaauwbroek.eu" messages: [ "*** WARNING ***" "This package will overwrite Coq's standard library files." "A backup of the original files will be placed under Coq's" "library directory at user-contrib/tactician-stdlib-backup/" "and they will be restored when you remove this package." "After installation of this package, all other Coq packages" "also need to be recompiled. Running the 'tactician recompile'" "command-line utility will help with this process." ] post-messages: [" --- The standard library was successfully recompiled --- In order to finish the process, you should run tactician recompile " {success}] depends: [ "coq" {>= "8.14" & < "8.15~"} "coq-tactician" ] build: [ [make "-j%{jobs}%"] ] install: [ [make "install"] ] remove: [ [make "restore"] ] url { src: "git+https://github.com/coq-tactician/coq-tactician-stdlib.git#coq8.14" } tags: [ "keyword:tactic-learning" "keyword:machine-learning" "keyword:automation" "keyword:proof-synthesis" "category:Miscellaneous/Coq Extensions" "logpath:Tactician" ]
true
Dry install with the current Coq version:
opam install -y --show-action coq-tactician-stdlib.8.14.dev coq.dev
[NOTE] Package coq is already installed (current version is dev). [ERROR] Package conflict! * No agreement on the version of coq: - coq >= dev - coq-tactician-stdlib = 8.14.dev -> coq < 8.15~ * No agreement on the version of ocaml: - (invariant) -> ocaml-base-compiler = 5.0.0 -> ocaml = 5.0.0 - coq-tactician-stdlib = 8.14.dev -> coq < 8.15~ -> ocaml < 4.05.0 You can temporarily relax the switch invariant with `--update-invariant' * No agreement on the version of ocaml-base-compiler: - (invariant) -> ocaml-base-compiler = 5.0.0 - coq-tactician-stdlib = 8.14.dev -> coq < 8.15~ -> ocaml < 4.05.0 -> ocaml-base-compiler = 3.08.3 * Incompatible packages: - (invariant) -> ocaml-base-compiler = 5.0.0 -> base-nnp - coq-tactician-stdlib = 8.14.dev -> coq < 8.15~ * Missing dependency: - coq-tactician-stdlib = 8.14.dev -> coq < 8.15~ -> ocaml < 4.05.0 -> ocaml-variants -> ocaml-beta unmet availability conditions: 'enable-ocaml-beta-repository' No solution found, exiting
Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
opam remove -y coq; opam install -y --show-action --unlock-base coq-tactician-stdlib.8.14.dev
true
true
No files were installed.
true