This repository presents an arithmetic library that is shared between several proof systems. For the moment, the proofs can be exported to the following systems:
Compiling the project
To compile the project, you need to install the last version of Dedukti https://github.com/Deducteam/Dedukti. The only dependency needed is
mongo that you can install with
opam. Then you can compile the project with
To export the library you can use the command
<system> can be either coq, matita. lean or pvs or opentheory. You can also compile all the files one:
to generate coq files for example.
Exporting the MongoDB Database
This process requires first to have a MongoDB server. You can install one with the following command:
sudo apt install mongodb
Then you need to run a server with the following command:
To export the Mongo DB, you just need to invoke the Makefile with the following command:
bdd folder, you will find scripts related to the bdd. In particular, since we are using MongoDB, it is better if you drop the old database before updating it.
- Lean/Coq/Matita/OpenTheory : François Thiré
- PVS : Gilles Dowek
- We don't use the functor mechanism of Coq for the moment because it is heavy to instantiate and hard to use.
- OpenTheory output comsumes a lot of memory (about 4Go). This is due to a memoization problem on our side. This should be fixed in a future version.
- Files are generated all at the same time. In later versions, we would like to generate them one by one.