Skip to content
Snippets Groups Projects

update build system and Iris

Merged 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

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
Please register or sign in to reply
Loading