package coq-tactician-stdlib
Recompiles Coq's standard libary with Tactician's instrumentation loaded
Install
Dune Dependency
Authors
Maintainers
Sources
1.0-beta1-8.13.tar.gz
sha512=6dd9eb3c81ef23604127619110fcf51ec268a15add6594337ae1031c42802a20d4b0ad28955831e2876372c748df54513cc14524872fd58439c453863cbd93e9
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
. Then exactly the same .vo
files are installed, except that they also contain Tactician's tactic databases.
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: 14 Jan 2021
Dependencies (2)
- coq-tactician
-
coq
>= "8.13" & < "8.14~"
Dev Dependencies
None
Used by
None
Conflicts
None
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page