2020-07-08 7:54:6 (GMT)
First clone veriT-rmx
git clone git@gitlab.inria.fr:hschurr/verit-rmx.git
cd verit-rmx
./configure
make -j
Then clone isabelle
hg clone http://isabelle.in.tum.de/repos/isabelle
cd isabelle
./bin/isabelle components -I
./bin/isabelle compenents -a
Then install veriT in Isabelle
vim ~/.isabelle/etc/settings
and add the lines
VERIT_HOME="/path/to/verit-rmx"
VERIT_SOLVER=$VERIT_HOME/veriT
Then activate the patches in mercurial
vim ~/.hgrc
In the extensions block add mq = (yes there is nothing right of the equality sign)
Finally clone the patches (Important: this will overwrite your own patches!)
cd /path/to/isabelle/.hg/patches
git pull git@gitlab.inria.fr:hschurr/isabelle-proof-dev.git
cd ../../
hg qpush f3_patch
Then you are ready to try the veriT reconstruction!
2020-07-08 8:28:27 (GMT)
Today is a Lean day for me. Maybe tomorrow, an Isabelle & Martin day. ;)
2020-07-08 8:29:49 (GMT)
Do you have a test case in Isabelle? Also, I don't see any recent change by you to Isabelle. Is that a good sign that things will work?
2020-07-08 10:38:31 (GMT)
No, I have not upstreamed my patches. They live in the git@gitlab.inria.fr:hschurr/isabelle-proof-dev.git repo. I have to test them on the AFP first. (Some things are missing, like supporting negative coefficients in the reconstruction of LIA).
2020-07-08 11:9:32 (GMT)
I got the invite now. :)