# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
conf-findutils 1 Virtual package relying on findutils
coq 8.12.2 Formal proof management system
num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.08.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.08.1 Official release 4.08.1
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.9.5 A library manager for OCaml
# opam file:
opam-version: "2.0"
name: "coq-tactician"
synopsis: "Tactician: A Seamless, Interactive Tactic Learner and Prover for Coq"
description: """
Tactician is a tactic learner and prover for the Coq Proof Assistant.
The system will help users make tactical proof decisions while they retain
control over the general proof strategy. To this end, Tactician will learn
from previously written tactic scripts, and either gives the user suggestions
about the next tactic to be executed or altogether takes over the burden of
proof synthesis. Tactician's goal is to provide the user with a seamless,
interactive, and intuitive experience together with strong, adaptive proof
automation.
"""
homepage: "https://coq-tactician.github.io"
dev-repo: "git+https://github.com/coq-tactician/coq-tactician"
bug-reports: "https://github.com/coq-tactician/coq-tactician/issues"
maintainer: "Lasse Blaauwbroek <lasse@blaauwbroek.eu>"
authors: "Lasse Blaauwbroek <lasse@blaauwbroek.eu"
depends: [
"ocaml" {>= "4.08"}
"dune" {>= "2.5"}
"opam-client" {>= "2.1.0~beta2"}
"cmdliner"
"coq" {>= "8.12" & < "8.13~"}
"coq-tactician-dummy"
]
depexts: ["git"]
build: [
["dune" "build" "--release" "-j" jobs]
]
post-messages: ["
--- Tactician was successfully installed ---
In order to enable Tactician, you should run
tactician enable
" {success}]
url {
src: "https://github.com/coq-tactician/coq-tactician/archive/1.0-beta1-8.12.tar.gz"
}
tags: [
"keyword:tactic-learning"
"keyword:machine-learning"
"keyword:automation"
"keyword:proof-synthesis"
"category:Miscellaneous/Coq Extensions"
"logpath:Tactician"
]
trueDry install with the current Coq version:
opam install -y --show-action coq-tactician.1.0~beta1+8.12 coq.8.12.2Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-tactician.1.0~beta1+8.12 coq.8.12.2opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-tactician.1.0~beta1+8.12 coq.8.12.2Total: 24 M
../ocaml-base-compiler.4.08.1/bin/tactician../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cma../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.a../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmxs../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Tactician/tactician_ltac1_record_plugin.cmxs../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Map_ssr_witnesses.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_things.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Ltacrecord.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cma../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_witnesses.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_annotate.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__G_ltac1_record.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmxs../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Tactician/tactician_ssreflect_plugin.cmxs../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.a../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Cook_tacexpr.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_subst_learner.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner_internal.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_substitute.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmxa../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Learner_helper.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Sexpr.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_things.cmti../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_normalize.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Known_ssr_witnesses.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner.cmti../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Known_witnesses.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/map_all_the_things.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Gendischarge.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/ltacrecord.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin__G_ltac1_tactics.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/g_ltac1_record.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Diagonal_iterative_search.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmxs../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Tactician/tactician_ltac1_tactics_plugin.cmxs../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Tactician/Ltac1/Record.vo../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Mapping_helpers.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactician_util.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Ltacrecord.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Timeouttac.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner_internal.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_substitute.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy_internal.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cma../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_things.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Ltacrecord.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy.cmti../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/map_ssr_witnesses.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Map_ssr_witnesses.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_normalize.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_annotate.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/dune-package../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.a../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner_internal.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmxa../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_substitute.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactic_annotate.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_normalize.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/map_all_the_witnesses.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_things.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Map_ssr_witnesses.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__G_ltac1_record.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__G_ltac1_record.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_annotate.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/cook_tacexpr.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Learner_helper.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Learner_helper.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/naiveknn_subst_learner.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Cook_tacexpr.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmxa../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Gendischarge.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin__G_ltac1_tactics.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_subst_learner.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin__G_ltac1_tactics.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Mapping_helpers.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Cook_tacexpr.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_witnesses.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Known_witnesses.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Known_ssr_witnesses.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Known_ssr_witnesses.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Known_witnesses.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_witnesses.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_subst_learner.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Mapping_helpers.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Sexpr.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/learner_helper.ml../ocaml-base-compiler.4.08.1/share/coq-tactician/coq-hott.8.11.patch../ocaml-base-compiler.4.08.1/share/coq-tactician/coq-hott.patch../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactic_learner_internal.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/sexpr.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/map_all_the_things.mli../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Sexpr.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy_internal.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Diagonal_iterative_search.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactician_util.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy_internal.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Diagonal_iterative_search.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Gendischarge.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Timeouttac.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Timeouttac.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactic_substitute.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactic_learner.mli../ocaml-base-compiler.4.08.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmt../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/known_ssr_witnesses.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/diagonal_iterative_search.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/tactics-plugin/g_ltac1_tactics.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/gendischarge.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactic_normalize.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/known_witnesses.ml../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Tactician/Ltac1/Record.v../ocaml-base-compiler.4.08.1/man/man1/tactician-enable.1../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Tactician/Ltac1/Tactics.vo../ocaml-base-compiler.4.08.1/man/man1/tactician.1../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactician_util.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/opam../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/timeouttac.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/META../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmx../ocaml-base-compiler.4.08.1/man/man1/tactician-recompile.1../ocaml-base-compiler.4.08.1/man/man1/tactician-eject.1../ocaml-base-compiler.4.08.1/man/man1/tactician-inject.1../ocaml-base-compiler.4.08.1/man/man1/tactician-disable.1../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactician_util.ml../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Tactician/Ltac1.vo../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Tactician/Ltac1/Tactics.v../ocaml-base-compiler.4.08.1/bin/tactician-patch../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/tactic_learner.ml../ocaml-base-compiler.4.08.1/doc/coq-tactician/LICENSE.md../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/search_strategy_internal.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmi../ocaml-base-compiler.4.08.1/bin/with-tactician../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/mapping_helpers.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/search_strategy.mli../ocaml-base-compiler.4.08.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmi../ocaml-base-compiler.4.08.1/lib/coq-tactician/record-plugin/search_strategy.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.ml../ocaml-base-compiler.4.08.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmx../ocaml-base-compiler.4.08.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.ml../ocaml-base-compiler.4.08.1/lib/coq/user-contrib/Tactician/Ltac1.v../ocaml-base-compiler.4.08.1/lib/coq-tactician/coqc.realopam remove -y coq-tactician.1.0~beta1+8.12