We need to pins to
- Ocaml base compiler to 4.13.1
- coq to 8.15.0,
directly run
dune build
We have pack all the coqc commnds into testshowcase.sh in FPOP directory.
The following commands are run under the FPOP
directory
We warn that, these tests are time consuming
cd FPOP
cat testshowcase.sh
The reader can directly try to run them via this shell file, and check output*.txt for the dump info.
Currently we cannot turn off the debug dump.
showcase_test/
includes all the showcase included in the papersrc/
andtheories/
includes all the source code of our plugin.LibTactics.v
andMaps.v
are directly from Software Foundation
src/familytype.ml
contains the main functionality of our plugin. For example, the internal data structure (representing family) and the translation from this internal data structure to Coq's command.src/fampoly.mlg
is the mlg file extending the Vernacular syntax for our pluginsrc/famprogram.ml
mainly interacts with the user. It contains the function thatfampoly.mlg
will invokesrc/fenv.ml
handles the environment/definitions of the families in our internal structuresrc/finduction.ml
implements theFRecursion
facilitysrc/finh.ml
implements the inheritance facilitysrc/ftheorem.ml
makes it possible to use proof script to work with our pluginsrc/utils
andsrc/CCCache.ml
are helpers.CCCache.ml
is directly copied fromOCaml-containers
(Thanks Simon Cruanes!)
- The debug dump will be generated during the usage of our plugin. We currently doesn't support turning it off
- Families have to be wrapped inside one module. (i.e. There has to be a very top level module, then we can define family inside this module)
- Not working well with VSCoq 0.3.8's "Interpret to End" Command. Because this command is actually interpreting the proof script in a parallel way. Current implementation breaks some of this assumption
- When running
coqc
on twoAnalysis_showcase
, it might took around 3 times the expected time. It won't immediately terminate after the final commandPrint Analysis_showcase.LangCP
. - VSCoq on MacOS is not working well with our plugin