update Iris for later credits

Should help with the nightly build failures. Unfortunately I cannot easily test this locally since the project does not seem to work with ProofGeneral out-of-the-box

Error: Cannot find a physical path bound to logical path type with prefix refinedc.typing.

Note sure what that is about. I see some _build things in _CoqProject. Maybe dune stuff? Anyway something that breaks the workflow I have been using for 10 years... so let's just see what CI says. ;)

(make builddep insists on installing cerberus which I don't want to do since I just want to change some Coq files.)

assigned to @jung

(Oh I now found this gem. I guess that's what I am missing. Arbitrary code execution by just dumping a file into $HOME. Great! Not something I will do though :) Isn't there some command I can just run by hand once to "make ProofGeneral work" that will generate the right _CoqProject or whatever? Or is PG + dune just such a bad combination still? Certainly good to know for Iris, looks like we won't switch to dune any time soon... sorry for the rant.^^

Ah, no CI for MRs, only on ci/ branches, I forgot we hadn't done that part of the setup here yet. Let me know if you want me to help set up CI for all MRs.

closed

mentioned in merge request !138 (merged)

Yeah, by default you can't rebuild stuff from PG. So you need to make sure that all the deps of your file have been built before you run the Coq toplevel in PG. To do that you can run dune build with a path to the file you want to build with extension .vo instead of .v.

I've actually added support for running a Coq toplevel in dune, which seems to work very well. But someone still needs to do the necessary changes in PG. (I won't do it myself since I hate emacs, and have no clue how to program it.)

(And the Coq project from the repo is correct for working with dune.)

Having imported files be built automatically is literally the main reason why I am still using PG+emacs, so giving that up is not really an option for me.^^ But I guess the people that maintain PG just aren't convinced by dune yet...

Anyway this is certainly good to know for my own decision making regarding whether to use dune or not for a Coq project. :)