Emilio Jesús Gallego Arias

An update on the current status, there are a few goals that would be great to have: - improved infrastructure for delaying proofs: as of now delaying a proof is...

We are getting some advances; main goal now is make `proof_entry` abstract, this will involve moving some code from `abstract` to declare, which seems like a very good thing to...

@herbelin recently re-took some missing parts of this roadmap and IMO the moment to think this bug can be closed is arriving, finally! There are very important post-mortem (in private...

@herbelin better let's discuss in private, but indeed I was talking of totally different issues that happened _after_ this issue was opened, not before.

> (test suite needs public_name for the exes it tests) We could also install private stuff in `libexec` binaries; I didn't do that as I'd like it to be better...

Much afraid nobody tackled on this, so it is 8.13 material now.

See also https://github.com/coq/www/pull/47

Amazing, I'm looking forward to play with it.

Great work @Zimmi48 , you could maybe look for opinions on your questions from some experienced members in the user community. Maybe @bcpierce00 and @andrew-appel would like to share some...

Thanks for the summary @Zimmi48 , indeed the main problem I see with HAL is that versioning is maybe not what you want for an artifact such as the manual,...