Erik Martin-Dorel

Just to confirm @hendriktews @Matafou Cc @cpitclaudel, the next PG-dev-telco slot is scheduled on Wed. 14 Apr. 21:00 CEST (same place as before); and as we said last time, let's...

Hi @sampollard @cpitclaudel, I didn't know `undo-tree` and I'm happy you could find a solution, but I'm afraid there might be some incompatibility all the same, given that ProofGeneral remaps...

Hi Stefan, thanks for your suggestion! > It can be fixed by replacing pg-protected-undo with an after-change-function which does the retraction (well, doing the retraction directly from after-change-function might be...

To be more precise, if one set `(setq proof-strict-read-only t)` with current PG master, start proving a lemma with several edits (to be undo-ed later), process its proof, and do...

@cpitclaudel > The fix shouldn't be too hard when proof-strict-read-only is nil. Yes, since setting `proof-strict-read-only = nil` just disables `pg-protected-undo`'s feature (and it's true that the code could be...

Thanks Stefan! :+1: so it indeed seems feasible to refactor the current implementation of the undo/revert feature, preserve the `proof-strict-read-only` semantics, and hopefully make it compatible with `undo-tree` :) as...

Hello, I fully agree with @hendriktews, all the more as the current protocol supported by Isabelle >2015 and by PG.master are strongly different (PIDE vs. REPL). So a "direct" update...

Hi @hendriktews, OK thanks for your reply; so I add this in my backlog.

Hi @palmskog (Cc @ppedrot), thanks for the ping > If we want to dig into the exact layout of the standard Coq Docker images and the filesizes we'll have to...

However I'd be wary of solutions that amounts to *building lighter images with `Print Assumptions` disabled or so*: IMHO the gain here would not be worth it the effort, given...