Skip to content

update build system and Iris

Ralf Jung requested to merge ralf/buildsystem into master

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.

Merge request reports