search

resource-reasoning / jscert_dev

This repository is now abandoned in favour of using
https://github.com/jscert/jscert
Other
0 stars 0 forks source link

Update TLC #10

Closed IgnoredAmbience closed 9 years ago

IgnoredAmbience commented 9 years ago

TLC now lives in git at https://gforge.inria.fr/git/tlc/tlc.git

Rebuilding old versions of jscert meet with TLC incompatibilities. We should move to a TLC submodule so that we have the library versioned.

charguer commented 9 years ago

Hi,

Just to mention, TLC now works with Coq 8.5. The version compatible with v8.4 can be found in the git history just before the merge of a branch called "coqbeta". Sorry I forgot to tell about it. Also, the svn of TLC is still alive, so old versions can be obtained from there.

Btw, Coq v8.5 seems to be working pretty well, so it could be good to try out the 8.5beta2 when it comes out. In particular, parallel coq compilation is now supported, it should vastly improve (re)compilation times.

Best, + Arthur

TLC now lives in git at https://gforge.inria.fr/git/tlc/tlc.git

Rebuilding old versions of jscert meet with TLC incompatibilities. We should move to a TLC submodule so that we have the library versioned.

— Reply to this email directly or view it on GitHub https://github.com/resource-reasoning/jscert_dev/issues/10.

IgnoredAmbience commented 9 years ago

My main reason for moving across to git was that I've been trying to reproduce the popl paper results, and have had a frustrating time just trying to get that version to build.

Having the precise version of tlc used at a point in time is very useful in this respect.

I've not yet looked at moving to Coq 8.5, but will eventually get around to looking through the changelog. Thanks for the info on the correct version of tlc for it!