Erik Martin-Dorel

Hi @ppedrot, yes I see what you mean; FTR: ```bash $ sudo docker run --rm -it mathcomp/mathcomp:1.15.0-coq-dev bash -c 'du -sh /home/coq/.opam/4.13.1+flambda/bin/* | sort -h' 0 /home/coq/.opam/4.13.1+flambda/bin/ocamlc 0 /home/coq/.opam/4.13.1+flambda/bin/ocamlcp 0...

:+1: @Zimmi48 Two related notes BTW: - just recalling that in a Dockerfile, adding `RUN sudo rm -f list_of_unneeded_files` does not lead to any space saving… (because of the layered-based...

> @erikmd : It took me a while to get the permissions and the environment right to run a test with a container from proofgeneral/coq-emacs. Do you have comments or...

Hi @hendriktews, thanks a lot for looking at this! and sorry for being less responsive… the Spring term is going to resume on Jan 4th so I'm extremely busy these...

BTW−FYI, I had already created (to save the name) a Docker Hub organization at URL https://hub.docker.com/u/proofgeneral, so we may use it for hosting some of these images :)

Thanks a lot @DavidAspinall for your fixup commits and for opening this issue! Actually I had spotted that the mailing lists were already down, so FYI after discussing with @Matafou...

BTW @DavidAspinall could you please attempt to backup/export the data from https://proofgeneral.inf.ed.ac.uk/trac (which did contain old issues and patches that may be useful for later reference), before the trac page...

Hi @HuStmpHrrr, thanks for the report! I can reproduce this with a fresh Emacs 25.1 as follows: ``` $ git clone https://github.com/melpa/melpa $ cd melpa $ make clean-packages clean-sandbox recipes/proof-general...

Excellent! thank you Stefan for the prompt fix :+1: I have redone the steps mentioned in [my comment](https://github.com/ProofGeneral/PG/issues/413#issuecomment-453782887) and it seems very OK. I guess we can close that issue....

Hi @monnier @cpitclaudel, FYI Stefan's fix 58cea1b8ffb02bc546ddb56a669d4094390d4809 was not enough to make `proof-general.el` work in all situations (in particular with [this proposed procedure](https://github.com/erikmd/tapfa-init.el#readme), where `use-package + proof-general` are installed at...