« Up

tactician dev 1 m 0 s 🏆

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                   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.1      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:
  "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."""
maintainer: ["Lasse Blaauwbroek <lasse@blaauwbroek.eu>"]
authors: ["Lasse Blaauwbroek <lasse@blaauwbroek.eu>"]
homepage: "https://coq-tactician.github.io"
bug-reports: "https://github.com/coq-tactician/coq-tactician/issues"
license: "MIT"
depends: [
  "dune" {>= "3.5" & < "3.8~"}
  "ocaml" {>= "4.08"}
  "dune-site" {>= "2.9.1"}
  "opam-client" {>= "2.1.0"}
  "cmdliner" {>= "1.1.0"}
  "coq-core" {= "dev"}
  "coq-stdlib" {= "dev" & with-test}
  "conf-git"
  "bos" {>= "0.2.1"}
  "coq-tactician-dummy" {= "8.17.dev" & with-test}
  "odoc" {with-doc}
]
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.git"
post-messages: ["
--- Tactician was successfully installed ---
In order to enable Tactician, you should run
tactician enable
" {success}]
tags: [
  "keyword:tactic-learning"
  "keyword:machine-learning"
  "keyword:automation"
  "keyword:proof-synthesis"
  "category:Miscellaneous/Coq Extensions"
  "logpath:Tactician"
]
substs: [
  "coq-shim/tactician-patch"
  "coq-shim/tactician.ml"
]
url {
  src: "git+https://github.com/coq-tactician/coq-tactician.git#coqdev"
}

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-tactician.dev coq.dev
Return code
0

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

Command
true
Return code
0

Install dependencies

Command
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-tactician.dev coq.dev
Return code
0
Duration
10 m 0 s

Install 🚀

Command
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y coq-tactician.dev coq.dev
Return code
0
Duration
1 m 0 s

Installation size

Total: 35 M

  • 19 M ../ocaml-base-compiler.4.14.0/bin/tactician
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cma
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.a
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmxs
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Tactician/tactician_ltac1_record_plugin.cmxs
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Map_ssr_witnesses.cmt
  • 817 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_things.cmt
  • 563 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cma
  • 549 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Ltacrecord.cmt
  • 298 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Monad_util.cmt
  • 269 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_witnesses.cmt
  • 264 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Features.cmt
  • 199 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_sexpr.cmt
  • 197 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_one_variable.cmt
  • 179 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_annotate.cmt
  • 178 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__G_ltac1_record.cmt
  • 177 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmxa
  • 165 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmxs
  • 165 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Tactician/tactician_ssreflect_plugin.cmxs
  • 160 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.a
  • 124 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Lshf_learner.cmt
  • 124 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner_internal.cmt
  • 124 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_subst_learner.cmt
  • 105 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_substitute.cmt
  • 104 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_abstract.cmt
  • 104 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Offline_evaluation_simulator_learner.cmt
  • 99 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_learner.cmt
  • 87 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Sexpr.cmt
  • 86 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Learner_helper.cmt
  • 84 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Inline_private_constants.cmt
  • 83 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_things.cmti
  • 77 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_normalize.cmt
  • 76 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactician_util.cmt
  • 72 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Cook_tacexpr.cmt
  • 71 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Find_tactic_syntax.cmt
  • 58 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_substitution_check_learner.cmt
  • 58 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Extreme_tactic_normalize.cmt
  • 57 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Trivial_learners.cmt
  • 52 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner.cmti
  • 51 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/map_all_the_things.ml
  • 51 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Benchmark.cmt
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin__G_ltac1_tactics.cmt
  • 48 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Diagonal_iterative_search.cmt
  • 47 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/ltacrecord.ml
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmxs
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Tactician/tactician_ltac1_tactics_plugin.cmxs
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/g_ltac1_record.ml
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Dijkstra_iterative_search.cmt
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Monad_util.cmi
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_one_variable.cmi
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Tactician/Ltac1/Record.vo
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Ltacrecord.cmi
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner_internal.cmi
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_abstract.cmi
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_substitute.cmi
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cma
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/features.ml
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmt
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/dune-package
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_things.cmi
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.a
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/ssreflect-plugin/map_ssr_witnesses.ml
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Ltacrecord.cmx
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner.cmt
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Mapping_helpers.cmt
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_sexpr.cmi
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Learner_helper.cmi
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_one_variable.cmx
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy_internal.cmt
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner.cmi
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Cook_tacexpr.cmi
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Find_tactic_syntax.cmi
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Map_ssr_witnesses.cmi
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_normalize.cmi
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Features.cmi
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Inline_private_constants.cmi
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Timeouttac.cmt
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner_internal.cmx
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_substitute.cmx
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_abstract.cmx
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_annotate.cmi
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Extreme_tactic_normalize.cmi
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_normalize.cmx
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_sexpr.cmx
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy.cmti
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_things.cmx
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Extreme_tactic_normalize.cmx
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Inline_private_constants.cmx
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/map_all_the_witnesses.ml
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactic_annotate.ml
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Monad_util.cmx
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Cook_tacexpr.cmx
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Find_tactic_syntax.cmx
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Offline_evaluation_simulator_learner.cmx
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Map_ssr_witnesses.cmx
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__G_ltac1_record.cmx
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Lshf_learner.cmi
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_learner.cmx
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Features.cmx
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__G_ltac1_record.cmi
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy.cmt
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/monad_util.ml
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_subst_learner.cmx
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_learner.cmi
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Learner_helper.cmx
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Lshf_learner.cmx
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmxa
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin__G_ltac1_tactics.cmx
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Offline_evaluation_simulator_learner.cmi
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_subst_learner.cmi
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Trivial_learners.cmx
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner.cmx
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin__G_ltac1_tactics.cmi
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Benchmark.cmi
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_annotate.cmx
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactic_sexpr.ml
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Benchmark.cmx
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactician_util.cmi
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactic_learner_internal.ml
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_substitution_check_learner.cmx
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/offline_evaluation_simulator_learner.ml
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_witnesses.cmx
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactician_util.cmx
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactic_one_variable.ml
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_substitution_check_learner.cmi
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Sexpr.cmx
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmxa
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/naiveknn_subst_learner.ml
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/map_all_the_things.mli
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_witnesses.cmi
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Diagonal_iterative_search.cmi
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Dijkstra_iterative_search.cmi
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/lshf_learner.ml
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Sexpr.cmi
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmi
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/sexpr.ml
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Diagonal_iterative_search.cmx
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Dijkstra_iterative_search.cmx
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Trivial_learners.cmi
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Mapping_helpers.cmi
  • 5 K ../ocaml-base-compiler.4.14.0/doc/coq-tactician/README.md
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.ml
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_util.ml
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Mapping_helpers.cmx
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/tactics-plugin/g_ltac1_tactics.ml
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy_internal.cmi
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy_internal.cmx
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/inline_private_constants.ml
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/naiveknn_learner.ml
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactic_substitution_check_learner.ml
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy.cmi
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/benchmark.ml
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy.cmx
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/learner_helper.ml
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/trivial_learners.ml
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/diagonal_iterative_search.ml
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Tactician/Ltac1/Record.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactic_learner.mli
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmt
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmt
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Tactician/Ltac1/Tactics.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/dijkstra_iterative_search.ml
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactic_normalize.ml
  • 2 K ../ocaml-base-compiler.4.14.0/man/man1/tactician.1
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/opam
  • 2 K ../ocaml-base-compiler.4.14.0/man/man1/tactician-enable.1
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmx
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/cook_tacexpr.ml
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactic_abstract.ml
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/find_tactic_syntax.ml
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactic_substitute.ml
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/META
  • 1 K ../ocaml-base-compiler.4.14.0/man/man1/tactician-eject.1
  • 1 K ../ocaml-base-compiler.4.14.0/man/man1/tactician-inject.1
  • 1 K ../ocaml-base-compiler.4.14.0/man/man1/tactician-disable.1
  • 1 K ../ocaml-base-compiler.4.14.0/man/man1/tactician-recompile.1
  • 1 K ../ocaml-base-compiler.4.14.0/doc/coq-tactician/LICENSE.md
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Tactician/Ltac1/Tactics.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/timeouttac.ml
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/extreme_tactic_normalize.ml
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactic_learner.ml
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Timeouttac.cmi
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Timeouttac.cmx
  • 1 K ../ocaml-base-compiler.4.14.0/share/coq-tactician/coq-hott.patch
  • 1 K ../ocaml-base-compiler.4.14.0/share/coq-tactician/coq-hott.8.15.patch
  • 1 K ../ocaml-base-compiler.4.14.0/share/coq-tactician/coq-hott.8.14.patch
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Tactician/Ltac1.vo
  • 1 K ../ocaml-base-compiler.4.14.0/share/coq-tactician/coq-hott.8.13.patch
  • 1 K ../ocaml-base-compiler.4.14.0/share/coq-tactician/coq-hott.8.12.patch
  • 1 K ../ocaml-base-compiler.4.14.0/share/coq-tactician/coq-hott.8.11.patch
  • 1 K ../ocaml-base-compiler.4.14.0/share/coq-tactician/coq-hott.8.10.patch
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/tactician-patch
  • 1 K ../ocaml-base-compiler.4.14.0/share/coq-tactician/coq-stdlib.patch
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/search_strategy_internal.ml
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/search_strategy.ml
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/search_strategy.mli
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/record-plugin/mapping_helpers.ml
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmi
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmi
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmx
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmx
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.ml
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.ml
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Tactician/Ltac1.v
  • 0 K ../ocaml-base-compiler.4.14.0/share/coq-tactician/plugins/coq-tactician/injection-flags
  • 0 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/coqtop.real
  • 0 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/coqidetop.real
  • 0 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/coqide.real
  • 0 K ../ocaml-base-compiler.4.14.0/lib/coq-tactician/coqc.real
  • 0 K ../ocaml-base-compiler.4.14.0/etc/coq-tactician/injection-flags

Uninstall 🧹

Command
opam remove -y coq-tactician.dev
Return code
0
Missing removes
none
Wrong removes
none

Sources are on GitHub © Guillaume Claret 🐣