-
- Downloads
There was a problem fetching the pipeline summary.
Merge branch 'ralf/buildsystem' into 'master'
update build system and Iris 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. See merge request !5
No related branches found
No related tags found
Pipeline #
Showing
- .gitignore 1 addition, 0 deletions.gitignore
- coq/ra/Makefile 6 additions, 11 deletionscoq/ra/Makefile
- coq/ra/adequacy.v 5 additions, 7 deletionscoq/ra/adequacy.v
- coq/ra/awk.Makefile 26 additions, 0 deletionscoq/ra/awk.Makefile
- coq/ra/base/ghosts.v 0 additions, 10 deletionscoq/ra/base/ghosts.v
- coq/ra/escrows.v 1 addition, 1 deletioncoq/ra/escrows.v
- coq/ra/examples/circ_buffer.v 1 addition, 1 deletioncoq/ra/examples/circ_buffer.v
- coq/ra/examples/message_passing.v 1 addition, 1 deletioncoq/ra/examples/message_passing.v
- coq/ra/examples/ticket_lock.v 1 addition, 1 deletioncoq/ra/examples/ticket_lock.v
- coq/ra/gps/inst_shared.v 1 addition, 1 deletioncoq/ra/gps/inst_shared.v
- coq/ra/gps/shared.v 2 additions, 5 deletionscoq/ra/gps/shared.v
- coq/ra/infrastructure.v 3 additions, 3 deletionscoq/ra/infrastructure.v
- coq/ra/persistor.v 1 addition, 1 deletioncoq/ra/persistor.v
- coq/ra/rsl.v 1 addition, 1 deletioncoq/ra/rsl.v
- opam.pins 1 addition, 1 deletionopam.pins
Loading
Please register or sign in to comment