ยซ Up

tactician dev 2 m 0 s ๐Ÿ†

Context

# Packages matching: installed
# Name                # Installed # Synopsis
base-bigarray         base
base-threads          base
base-unix             base
conf-findutils        1           Virtual package relying on findutils
conf-gmp              4           Virtual package relying on a GMP lib system installation
coq                   dev         Formal proof management system
dune                  3.1.1       Fast, portable, and opinionated build system
ocaml                 4.12.1      The OCaml compiler (virtual package)
ocaml-base-compiler   4.12.1      Official release 4.12.1
ocaml-config          2           OCaml Switch Configuration
ocaml-options-vanilla 1           Ensure that OCaml is compiled with no special options enabled
ocamlfind             1.9.3       A library manager for OCaml
zarith                1.12        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"
depends: [
  "ocaml" {>= "4.08"}
  "dune" {>= "2.8"}
  "dune-site" {>= "2.9.1"}
  "opam-client" {>= "2.1.0~beta2"}
  "cmdliner"
  "coq" {= "dev"}
  "conf-git"
  "bos" {>= "0.2.1"}
  "coq-tactician-dummy" {= "dev" & with-test}
  "odoc" {with-doc}
]
build: [
  ["dune" "subst"] {dev}
  [
    "dune"
    "build"
    "-p"
    name
    "-j"
    jobs
    "@install"
    "@runtest" {with-test}
    "@doc" {with-doc}
  ]
]
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
7 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
2 m 0 s

Installation size

Total: 36 M

  • 20 M ../ocaml-base-compiler.4.12.1/bin/tactician
  • 2 M ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cma
  • 2 M ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.a
  • 2 M ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmxs
  • 2 M ../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Tactician/tactician_ltac1_record_plugin.cmxs
  • 1008 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Map_ssr_witnesses.cmt
  • 799 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_things.cmt
  • 474 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cma
  • 448 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Ltacrecord.cmt
  • 290 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Monad_util.cmt
  • 264 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Features.cmt
  • 233 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_witnesses.cmt
  • 203 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_one_variable.cmt
  • 200 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_sexpr.cmt
  • 183 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_annotate.cmt
  • 177 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmxa
  • 175 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmxs
  • 175 K ../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Tactician/tactician_ssreflect_plugin.cmxs
  • 174 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__G_ltac1_record.cmt
  • 167 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.a
  • 147 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Cook_tacexpr.cmt
  • 145 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_subst_learner.cmt
  • 127 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Lshf_learner.cmt
  • 117 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner_internal.cmt
  • 111 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Offline_evaluation_simulator_learner.cmt
  • 108 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_substitute.cmt
  • 108 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_abstract.cmt
  • 97 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_learner.cmt
  • 84 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Learner_helper.cmt
  • 82 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Sexpr.cmt
  • 80 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Inline_private_constants.cmt
  • 78 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_normalize.cmt
  • 78 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_things.cmti
  • 74 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Find_tactic_syntax.cmt
  • 73 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactician_util.cmt
  • 60 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Extreme_tactic_normalize.cmt
  • 59 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_substitution_check_learner.cmt
  • 57 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Known_ssr_witnesses.cmt
  • 57 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Trivial_learners.cmt
  • 51 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner.cmti
  • 51 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Benchmark.cmt
  • 49 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/map_all_the_things.ml
  • 49 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Known_witnesses.cmt
  • 42 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Gendischarge.cmt
  • 39 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/g_ltac1_record.ml
  • 39 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin__G_ltac1_tactics.cmt
  • 37 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/ltacrecord.ml
  • 37 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Monad_util.cmi
  • 36 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmxs
  • 36 K ../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Tactician/tactician_ltac1_tactics_plugin.cmxs
  • 34 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Diagonal_iterative_search.cmt
  • 33 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_one_variable.cmi
  • 28 K ../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Tactician/Ltac1/Record.vo
  • 25 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Ltacrecord.cmi
  • 25 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_abstract.cmi
  • 25 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner_internal.cmi
  • 24 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_substitute.cmi
  • 23 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/features.ml
  • 22 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmt
  • 21 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_things.cmi
  • 19 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Timeouttac.cmt
  • 19 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/dune-package
  • 19 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner.cmt
  • 19 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cma
  • 19 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Learner_helper.cmi
  • 19 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_sexpr.cmi
  • 19 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Mapping_helpers.cmt
  • 19 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_one_variable.cmx
  • 18 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Ltacrecord.cmx
  • 17 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner.cmi
  • 17 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/ssreflect-plugin/map_ssr_witnesses.ml
  • 17 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy_internal.cmt
  • 16 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Find_tactic_syntax.cmi
  • 16 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Map_ssr_witnesses.cmi
  • 16 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.a
  • 15 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_normalize.cmi
  • 15 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Features.cmi
  • 15 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Inline_private_constants.cmi
  • 14 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_substitute.cmx
  • 14 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_abstract.cmx
  • 14 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_annotate.cmi
  • 14 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner_internal.cmx
  • 14 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Extreme_tactic_normalize.cmi
  • 14 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmxa
  • 14 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_sexpr.cmx
  • 13 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_normalize.cmx
  • 12 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactic_annotate.ml
  • 12 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy.cmti
  • 12 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Monad_util.cmx
  • 12 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Extreme_tactic_normalize.cmx
  • 12 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Inline_private_constants.cmx
  • 11 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_things.cmx
  • 11 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Find_tactic_syntax.cmx
  • 11 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_subst_learner.cmx
  • 11 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Lshf_learner.cmi
  • 11 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_subst_learner.cmi
  • 10 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/map_all_the_witnesses.ml
  • 10 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__G_ltac1_record.cmx
  • 10 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Offline_evaluation_simulator_learner.cmx
  • 10 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Features.cmx
  • 10 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Map_ssr_witnesses.cmx
  • 10 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_learner.cmx
  • 9 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/monad_util.ml
  • 9 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__G_ltac1_record.cmi
  • 9 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Naiveknn_learner.cmi
  • 9 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy.cmt
  • 9 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Lshf_learner.cmx
  • 9 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Learner_helper.cmx
  • 9 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Trivial_learners.cmx
  • 8 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactic_sexpr.ml
  • 8 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmxa
  • 8 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Offline_evaluation_simulator_learner.cmi
  • 8 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin__G_ltac1_tactics.cmx
  • 8 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_witnesses.cmx
  • 8 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_learner.cmx
  • 8 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactic_one_variable.ml
  • 8 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/cook_tacexpr.ml
  • 8 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Benchmark.cmi
  • 8 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Known_ssr_witnesses.cmx
  • 8 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin__G_ltac1_tactics.cmi
  • 8 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin__Known_ssr_witnesses.cmi
  • 8 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Known_witnesses.cmx
  • 8 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Gendischarge.cmi
  • 8 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Known_witnesses.cmi
  • 8 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_annotate.cmx
  • 7 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Map_all_the_witnesses.cmi
  • 7 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Benchmark.cmx
  • 7 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/offline_evaluation_simulator_learner.ml
  • 7 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactic_learner_internal.ml
  • 7 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactician_util.cmi
  • 7 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_substitution_check_learner.cmx
  • 7 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Sexpr.cmx
  • 6 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Cook_tacexpr.cmi
  • 6 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactic_substitution_check_learner.cmi
  • 6 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Tactician_util.cmx
  • 6 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/naiveknn_subst_learner.ml
  • 6 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/lshf_learner.ml
  • 6 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Cook_tacexpr.cmx
  • 6 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/map_all_the_things.mli
  • 6 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmi
  • 6 K ../ocaml-base-compiler.4.12.1/share/coq-tactician/coq-hott.8.11.patch
  • 6 K ../ocaml-base-compiler.4.12.1/share/coq-tactician/coq-hott.patch
  • 5 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Sexpr.cmi
  • 5 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Diagonal_iterative_search.cmi
  • 5 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/sexpr.ml
  • 5 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Trivial_learners.cmi
  • 5 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Mapping_helpers.cmi
  • 5 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.ml
  • 5 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Diagonal_iterative_search.cmx
  • 4 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy_internal.cmx
  • 4 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Mapping_helpers.cmx
  • 4 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_util.ml
  • 4 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy_internal.cmi
  • 4 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Gendischarge.cmx
  • 4 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/inline_private_constants.ml
  • 4 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/naiveknn_learner.ml
  • 4 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactic_substitution_check_learner.ml
  • 4 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy.cmx
  • 4 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Search_strategy.cmi
  • 3 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/benchmark.ml
  • 3 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/learner_helper.ml
  • 3 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmt
  • 3 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/trivial_learners.ml
  • 3 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Timeouttac.cmi
  • 3 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin__Timeouttac.cmx
  • 3 K ../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Tactician/Ltac1/Record.v
  • 3 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactic_learner.mli
  • 3 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmt
  • 3 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactic_normalize.ml
  • 3 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/tactics-plugin/g_ltac1_tactics.ml
  • 2 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactic_abstract.ml
  • 2 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/ssreflect-plugin/known_ssr_witnesses.ml
  • 2 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/diagonal_iterative_search.ml
  • 2 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactic_substitute.ml
  • 2 K ../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Tactician/Ltac1/Tactics.vo
  • 2 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/find_tactic_syntax.ml
  • 2 K ../ocaml-base-compiler.4.12.1/man/man1/tactician.1
  • 2 K ../ocaml-base-compiler.4.12.1/man/man1/tactician-enable.1
  • 2 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactician_ltac1_record_plugin.cmx
  • 2 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/opam
  • 2 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/gendischarge.ml
  • 2 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/known_witnesses.ml
  • 1 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/timeouttac.ml
  • 1 K ../ocaml-base-compiler.4.12.1/man/man1/tactician-recompile.1
  • 1 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/extreme_tactic_normalize.ml
  • 1 K ../ocaml-base-compiler.4.12.1/man/man1/tactician-eject.1
  • 1 K ../ocaml-base-compiler.4.12.1/man/man1/tactician-inject.1
  • 1 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/META
  • 1 K ../ocaml-base-compiler.4.12.1/man/man1/tactician-disable.1
  • 1 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/tactic_learner.ml
  • 1 K ../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Tactician/Ltac1/Tactics.v
  • 1 K ../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Tactician/Ltac1.vo
  • 1 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/tactician-patch
  • 1 K ../ocaml-base-compiler.4.12.1/doc/coq-tactician/LICENSE.md
  • 1 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmi
  • 1 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/search_strategy_internal.ml
  • 1 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/mapping_helpers.ml
  • 1 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/search_strategy.mli
  • 1 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmi
  • 1 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/record-plugin/search_strategy.ml
  • 1 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.ml
  • 1 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/ssreflect-plugin/tactician_ssreflect_plugin.cmx
  • 1 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.cmx
  • 1 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/tactics-plugin/tactician_ltac1_tactics_plugin.ml
  • 1 K ../ocaml-base-compiler.4.12.1/lib/coq/user-contrib/Tactician/Ltac1.v
  • 0 K ../ocaml-base-compiler.4.12.1/etc/coq-tactician/injection-flags
  • 0 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/coqc.real
  • 0 K ../ocaml-base-compiler.4.12.1/lib/coq-tactician/coqtop.real
  • 0 K ../ocaml-base-compiler.4.12.1/share/coq-tactician/plugins/coq-tactician/injection-flags

Uninstall ๐Ÿงน

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