iGPS merge requestshttps://gitlab.mpi-sws.org/FP/igps/-/merge_requests2017-11-14T15:37:50Zhttps://gitlab.mpi-sws.org/FP/igps/-/merge_requests/14Get rid of `%C` scopes.2017-11-14T15:37:50ZRobbert KrebbersGet rid of `%C` scopes.As already done at most places, only open `uPred_scope` around definitions. That way there is no need for `%C` scopes in lemmas anymore.As already done at most places, only open `uPred_scope` around definitions. That way there is no need for `%C` scopes in lemmas anymore.https://gitlab.mpi-sws.org/FP/igps/-/merge_requests/13test against released Coq 8.7.02017-10-30T09:35:20ZRalf Jungjung@mpi-sws.orgtest against released Coq 8.7.0https://gitlab.mpi-sws.org/FP/igps/-/merge_requests/12use strongly_atomic from Iris2017-10-30T09:02:24ZRalf Jungjung@mpi-sws.orguse strongly_atomic from IrisTo be honest I do not understand why you need it, but whatever.To be honest I do not understand why you need it, but whatever.https://gitlab.mpi-sws.org/FP/igps/-/merge_requests/11update README2017-09-25T13:41:01ZRalf Jungjung@mpi-sws.orgupdate READMEhttps://gitlab.mpi-sws.org/FP/igps/-/merge_requests/10make it compatible with Coq 8.7, and test that2017-09-25T12:02:41ZRalf Jungjung@mpi-sws.orgmake it compatible with Coq 8.7, and test thatTurns out Coq 8.7 is 20% faster. :-) Some of this is lost to parallelism though, it seems.
8.6:
```
real 11m7.102s
user 25m5.797s
sys 0m17.457s
```
8.7:
```
real 9m0.417s
user 19m40.020s
sys 0m16.213s
```
I reported t...Turns out Coq 8.7 is 20% faster. :-) Some of this is lost to parallelism though, it seems.
8.6:
```
real 11m7.102s
user 25m5.797s
sys 0m17.457s
```
8.7:
```
real 9m0.417s
user 19m40.020s
sys 0m16.213s
```
I reported the fact that I had to change something to make it work again as <https://coq.inria.fr/bugs/show_bug.cgi?id=5749>.https://gitlab.mpi-sws.org/FP/igps/-/merge_requests/9Make directory layout match other iris projects2017-08-26T20:15:17ZRalf Jungjung@mpi-sws.orgMake directory layout match other iris projectsYay for more uniformity :)Yay for more uniformity :)https://gitlab.mpi-sws.org/FP/igps/-/merge_requests/8CI: test against coq 8.6.12017-08-22T13:22:09ZRalf Jungjung@mpi-sws.orgCI: test against coq 8.6.1https://gitlab.mpi-sws.org/FP/igps/-/merge_requests/7Update build & CI files to properly use new CI machine2017-03-14T10:00:44ZRalf Jungjung@mpi-sws.orgUpdate build & CI files to properly use new CI machineThe title says it all. I have to say your unconventional directory layout (in particular, not using a `theories` folder) makes it more annoying than it would have to be to update your build system. ;)
If you tell me there's currently no...The title says it all. I have to say your unconventional directory layout (in particular, not using a `theories` folder) makes it more annoying than it would have to be to update your build system. ;)
If you tell me there's currently no branch somewhere that would break, I'd be happy to introduce a `theories` folder for you. That would mostly involve `git mv coq/ra coq/theories` as well as moving `Makefile` and `_CoqProject` one folder up, i.e., directly into `coq/`.https://gitlab.mpi-sws.org/FP/igps/-/merge_requests/6awk.Makefile: improve uninstall target2017-01-12T21:16:51ZRalf Jungjung@mpi-sws.orgawk.Makefile: improve uninstall targetThis uninstalls enough things to actually uninstall everything that is installed by "make install". It also gets rid of the fragile manual configuration of the folder that stuff is uninstalled from and uses awk magic instead.This uninstalls enough things to actually uninstall everything that is installed by "make install". It also gets rid of the fragile manual configuration of the folder that stuff is uninstalled from and uses awk magic instead.https://gitlab.mpi-sws.org/FP/igps/-/merge_requests/5update build system and Iris2017-01-09T14:44:15ZRalf Jungjung@mpi-sws.orgupdate build system and IrisThis makes "make vio2vo J=X" first call "make quick", and the target is incremental so it will do less useless work.
This also fixes a bug in "make uninstall".
Finally, it uses the new solve_inG tactic, mainly to make sure that the tac...This makes "make vio2vo J=X" first call "make quick", and the target is incremental so it will do less useless work.
This also fixes a bug in "make uninstall".
Finally, it uses the new solve_inG tactic, mainly to make sure that the tactic is actually general enough.
I remove the "foundational\Sigma" indirection to make GPS more consistent with the usual style of Iris, which is to have one "subG -> inG" instance for every \Sigma. The tactic also assumes this, which is why I noticed. Also, `constRF` recently became a coercion.https://gitlab.mpi-sws.org/FP/igps/-/merge_requests/3use opam-based CI2017-01-05T15:33:39ZRalf Jungjung@mpi-sws.orguse opam-based CIThis switches the CI to use opam to build dependencies -- the only mode that will be supported on the new CI machine. opam is also used to cache build dependencies, so we no longer rely on keeping old files in the CI directory. (The buil...This switches the CI to use opam to build dependencies -- the only mode that will be supported on the new CI machine. opam is also used to cache build dependencies, so we no longer rely on keeping old files in the CI directory. (The build mode can be set to "git clone" once this is merged.) It is also trivial now to change the Coq version that is used. If you want, I can add a second job that builds GPS against Coq 8.6.dev (the current revision of the 8.6 branch), or we could even entirely ditch Coq 8.5 and build only against 8.6.dev. (Iris is currently tested against both 8.5.3 and 8.6.dev; we will use the dev version only until 8.6 is released, of course.) You can also easily use `make quick && make vio2vo` or so instead of just `make` because this no longer needs Iris to be built the same way.
There are two observable differences for the user:
* No more iris submodule. Instead, the file opam.pins tracks the git commit of Iris that is to be used. As a user, `make build-dep` will use opam to install and/or upgrade everything you need (Coq, ssreflect, Iris) in the right version. Of course you can still do `make install` in Iris manually if you don't want to or can't use opam.
* No more separate stages for updating build-deps and building GPS itself. If you really want to keep those separate, I can make that happen, but it will overall slow things down because the cache has to be copied back and forth. (Also, it may break if we ever have two CI runners.)
TODOs:
* Which name should this project have in opam? I picked `coq-gps`.
* I didn't know of any homepage for this project so currently, opam doesn't give any.
* The folder structure is somewhat weird because unlike the other projects, `Makefile` and `_CoqProject` are in the same folder that is mapped as library folder for Coq. I made things work by adding a `cd` here and there, but the nicer thing to do would be to rename `coq/ra` to `coq/theories` and move `Makefile` and `_CoqProject` up into `coq`.
* Currently, if you `make install` this project, stuff is installed to a folder `ra`. This is determined by the first line in `_CoqProject`. It should probably be changed (and then the `opam` file also needs changing because it uninstalls things by deleting that directory).
Cc @janno @haidanghttps://gitlab.mpi-sws.org/FP/igps/-/merge_requests/4Resolve "Typo in appendix's circular buffer example"2016-12-20T14:31:47ZHai DangResolve "Typo in appendix's circular buffer example"Closes #2Closes #2https://gitlab.mpi-sws.org/FP/igps/-/merge_requests/2Coq8.6 is also compatible with 8.5 - make it the new master2016-12-07T20:55:34ZJannoCoq8.6 is also compatible with 8.5 - make it the new master[No text][No text]JannoJannohttps://gitlab.mpi-sws.org/FP/igps/-/merge_requests/1the Coq CI image now contains git2016-11-07T12:38:37ZRalf Jungjung@mpi-sws.orgthe Coq CI image now contains gitI added git to the Coq CI image, only to then notice it seems you already did that. If adding git is the *only* difference in the `coq-git` image, we can get rid of that image.
Cc @jannoI added git to the Coq CI image, only to then notice it seems you already did that. If adding git is the *only* difference in the `coq-git` image, we can get rid of that image.
Cc @janno