Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

emacs eats up all my RAM while processing imports #499

Closed
RalfJung opened this issue Jun 10, 2020 · 22 comments · Fixed by #503
Closed

emacs eats up all my RAM while processing imports #499

RalfJung opened this issue Jun 10, 2020 · 22 comments · Fixed by #503

Comments

@RalfJung
Copy link

I am having trouble using PG on a particular Coq development, where when I step over the Require commands at the top of the file it never completes, instead eating up all of my RAM until the machine starts thrashing. When I killed it the emacs process was at more than 80% of my 16GB RAM. Running make in the same project to build it all with coqc works fine.

To reproduce, clone https://github.com/mit-pdos/perennial, initialize submodules (git submodule update --init --recursive), and then open pretty much any file and step to the end of the buffer in PG. I tried external/Goose/github_com/mit_pdos/perennial_examples/replicated_block.v and src/program_logic/crash_weakestpre.v.

This is with latest PG master and emacs 1:26.3+1-2 on Debian testing.

@RalfJung
Copy link
Author

Curiously, in src/program_logic/crash_weakestpre.v, when I step over each line individually it works fine. But when I step to the bottom of the file at once, it goes crazy.

@cpitclaudel
Copy link
Member

Any chance you could collect a memory profile? M-x profiler-start, select mem, open and reproduce the issue, then M-x profiler-report and M-x profiler-report-write-profile

@RalfJung
Copy link
Author

open and reproduce the issue, then M-x profiler-report

emacs is unresponsive once the RAM usage skyrockets and I have to send it a SIGKILL. So, I can't run any more M-x commands at that point I am afraid...

@RalfJung
Copy link
Author

I'm happy to throw other debuggers at it though if you know anything that could be useful.^^

@monnier
Copy link
Contributor

monnier commented Jun 10, 2020 via email

@hendriktews
Copy link
Collaborator

hendriktews commented Jun 10, 2020 via email

@RalfJung
Copy link
Author

does this happen with the default Proof General customization? Do
you have any auto-compilation features enabled?

Good idea! When I remove the "customization" block, the bug goes away. I'll try to bisect which is the "bad" option.

When I try (with auto vos compilation) I immediately see an error
about some library not being in the load path and nothing goes
crazy, but I probably have a completely different Proof General
customization.

Did you do the submodule init? Also, does it help to run make on the console first? Which Coq version are you using?

@RalfJung
Copy link
Author

RalfJung commented Jun 11, 2020

So the problem is this line:

'(coq-compile-before-require t)

When I comment this out, it all works. But of course, I quite like this feature...

Here are my other coq/proof-related settings:

 '(coq-compile-parallel-in-background t)
 '(coq-compile-quick (quote no-quick))
 '(coq-one-command-per-line nil)
 '(proof-follow-mode (quote followdown))
 '(proof-next-command-insert-space nil)
 '(proof-splash-enable nil)
 '(proof-three-window-enable t)

@hendriktews
Copy link
Collaborator

I am sorry, I cannot reproduce. I did

git clone  https://github.com/mit-pdos/perennial
cd perennial/
git submodule update --init --recursive
make -j 4 src/program_logic/crash_weakestpre.vo
emacs -q -l ~/src/pg/499.el src/program_logic/crash_weakestpre.v

with 499.el containing

(setq coq-compile-parallel-in-background t
      coq-compile-quick (quote no-quick)
      coq-one-command-per-line nil
      proof-follow-mode (quote followdown)
      proof-next-command-insert-space nil
      proof-splash-enable nil
      proof-three-window-enable t)

(load-file (expand-file-name "~/src/pg/master/generic/proof-site.el"))

In src/program_logic/crash_weakestpre.v I go to the bottom and
do C-c C-return. It takes a while, but eventually asserts
everything. Nothing goes crazy.

At ~/src/pg/master I am at 5c3ebac1 New hook for early prompt/output analyzis. I use Coq 8.11.1.

Please provide more detailed instructions, preferably for a file
for which compilation takes less time.

And please do answer all the questions, in particular the one
about the *Messages* buffer.

@RalfJung
Copy link
Author

RalfJung commented Jun 12, 2020

a file for which compilation takes less time

As mentioned before, external/Goose/github_com/mit_pdos/perennial_examples/replicated_block.v also shows this behavior. My guess is that all files do. (EDIT: Ah but that file also takes a while, sorry.)

I am using coq.8.12.dev from opam. I'll see if using a different Coq version makes a difference. I'll also try to minimize my .emacs file so that I can share it.

I tried getting the *Messages* buffer, but unfortunately it is impossible: what I do is I open both that buffer and the Coq file side-by-side, and then C-c C-Return in the Coq file. But then it changes the window layout to the PG one (with the 3 buffers for file, goal, Coq output), hiding *Messages*, and then emacs freezes up and I cannot switch buffers any more.

@RalfJung
Copy link
Author

RalfJung commented Jun 12, 2020

@hendriktews

I cannot reproduce

Looks like you did not set the one setting which I identified as problematic above, coq-compile-before-require.

Please provide more detailed instructions

Here's the minimal .emacs:

;; Custom (managed) Settings
(custom-set-variables
 ;; custom-set-variables was added by Custom.
 ;; If you edit it by hand, you could mess it up, so be careful.
 ;; Your init file should contain only one such instance.
 ;; If there is more than one, they won't work right.
 '(coq-compile-before-require t))

;; Coq
(load "~/src/coq/ProofGeneral/generic/proof-site.el")

With that file, the following reproduces the problem, using Coq 8.11.2 from opam:

git clone  https://github.com/mit-pdos/perennial
cd perennial/
git submodule update --init --recursive
make -j8 external/Goose/github_com/mit_pdos/perennial_examples/replicated_block.vo
emacs external/Goose/github_com/mit_pdos/perennial_examples/replicated_block.v

In emacs, I got to the bottom of the file and do C-c C-Return.

This still takes a while to build, and interestingly it's not all files that are broken. I'll walk up the dependency chain.

@RalfJung
Copy link
Author

RalfJung commented Jun 12, 2020

When you open the Messages buffer in a second frame, do you see
any pattern of messages scrolling by?

I managed to see something in that buffer by disabling "Toggle 3 Windows Mode" in the Coq menu. A lot of things scroll by faster than I can read; when things freeze, it looks as follows:

Screenshot_20200612_134003

@RalfJung
Copy link
Author

RalfJung commented Jun 12, 2020

Here's something strange:

rm external/iris/_CoqProject # needed to make PG pick up the right _CoqProject file
emacs external/iris/theories/base_logic/lib/fancy_updates.v

This doesn't eat up all my RAM, but it tops out at 11% of my 16GB of RAM. When I open the same file in a separate clone of Iris, RAM usage is much lower. For external/iris/theories/program_logic/weakestpre.v, it tops at 20%.

Looks like the further I go up the dependency chain, the smaller RAM usage becomes, but it's still way bigger than I would expect.

One thing that is peculiar about the perennial repository is that it's a ton of files that are all built in one makefile. The overall dependency graph is rather big. So maybe this is not PG going into an infinite loop, maybe this is just exposing that PG is wasting a lot of RAM on dependency tracking, and this repository is big enough to actually make that a problem?

@hendriktews
Copy link
Collaborator

Thanks for your patience, I can now reproduce with program_logic/crash_weakestpre. And thanks for spotting that I forgot about the crucial option. Your suggestion replicated_block does not work here, because make fails on it. I can reproduce with only asserting the first two lines of crash_weakestpre. For them PG processes around 400 dependencies only, until I interrupt it with C-g. I therefore don't believe the amount of dependencies is the problem.

@hendriktews
Copy link
Collaborator

It will take a while to debug this. What I can see now is that the problem immediately starts with processing the coqdep output of external/iris/theories/base_logic/upred.v. Is there anything special with that file?

Meanwhile I have another question: Does the makefile also generate coq project files? Because, when I process some imports in a fresh checkout, it immediately fails, because libraries cannot be found. I would guess now, that the load path is incomplete, maybe, because the project files are not there yet?

@hendriktews
Copy link
Collaborator

With some more debug output the problems start one file earlier at external/stdpp/theorie/proof_irrel.v, it has probably nothing to do with the files.

@RalfJung
Copy link
Author

What I can see now is that the problem immediately starts with processing the coqdep output of external/iris/theories/base_logic/upred.v. Is there anything special with that file?

Hm, not that I know of.

Meanwhile I have another question: Does the makefile also generate coq project files?

Looks like the topmost _CoqProject is generated by the Makefile, yes. Cc @tchajed

@hendriktews
Copy link
Collaborator

hendriktews commented Jun 14, 2020 via email

@tchajed
Copy link
Contributor

tchajed commented Jun 14, 2020

We do have a weird setup where the dependencies are hooked into a single tree and then we have a custom Makefile that just uses coqdep and has its own compilation rule. One issue this does raise is that there are multiple _CoqProject files, and only the root one should be used (which is what the Makefile does).

@RalfJung if your hypothesis is right that it's just the magnitude of the dependencies, you could try disabling compiling the large ones with this:

(setq coq-compile-ignored-directories
      '("external/iris/.*" "external/stdpp/.*" "external/coqutil/.*"))

@hendriktews
Copy link
Collaborator

hendriktews commented Jun 14, 2020

I found the problem: It's the naive way of propagating ancestors upwards in the dependency tree. When I programmed this, I simply appended all ancestors of all dependees - this leads to an exponential duplication of ancestors in tightly coupled dependency graphs.

If you want a quick solution, replace

  (let ((ancestors (get job 'ancestors))

in function coq-par-kickoff-coqc-dependants in coq-par-compile.el with

  (let ((ancestors (and coq-lock-ancestors (get job 'ancestors)))

and disable coq-lock-ancestors.

I will replace the lists with a hash, I guess.

@RalfJung
Copy link
Author

@hendriktews that patch and the config change does it, thanks a lot. :)

hendriktews added a commit to hendriktews/PG that referenced this issue Jun 19, 2020
The hash avoids an exponentially growing number of duplicates in
the ancestor collection. Fixes ProofGeneral#499
@RalfJung
Copy link
Author

I can confirm that this fixes the problem, thanks a lot :)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

6 participants