package coq-tactician-stdlib
Recompiles Coq's standard libary with Tactician's instrumentation loaded
Install
Dune Dependency
Authors
Maintainers
Sources
1.0-beta2-8.15.tar.gz
sha512=0add94573cfb435a4e0f7bb87a472e220416197bc8375ebf0b0c92d7d8f8adc57f034d4ddafd443516db4930bea54fc3d3f4b7bd1e4e7249a90dfb47de6da085
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.
Tags
keyword:tactic-learning keyword:machine-learning keyword:automation keyword:proof-synthesis category:Miscellaneous/Coq Extensions logpath:TacticianPublished: 20 Oct 2023
Dependencies (2)
- coq-tactician
-
coq
>= "8.15" & < "8.16~"
Dev Dependencies
None
Used by
None
Conflicts
None
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page