6

I've been working in an Isabelle 2019 session which has grown a bit large, and at some point I wasn't able to build it anymore using isabelle build in my 8G RAM machine. Nevertheless, when I open the main theory file using jEdit (running isabelle jedit -d .), the session is built with no problems.

How can I tune the building process so it works as smoothly as the graphical interface?

Next, I give some more details.

The main symptom is that the Poly/ML process stalls at some point; it doesn't really fail but does not terminate within a reasonable amount of time (~20min, when a successful build would take 3' in my computer).

Amidst of the development, adjusting using ML_OPTIONS to "--minheap 5500" was enough to solve this, but afterwards we decided to split the session in two (no more code added, just a change in the ROOT file) and after that no further adjustment solved the issue. On the other hand, a machine with 16G RAM builds with no problem without any further setting.

EDIT. I've checked the options used by jEdit; those relevant (I believe) are --minheap 500 --gcthreads 0 (the last being a default). I tried with these with no success. I also noted that the build command has a distinct --eval Command_Line.tool0 (fn () => (Build.build "/tmp/isabelle-pedro/buildNNNNNNNNNNNNN")) option, where NNNNNNNNNNNNN are some numbers.

Pedro Sánchez Terraf
  • 231
  • 1
  • 7
  • Perhaps this is related to this [old Poly/ML behaviour](https://polyml.inf.ed.ac.narkive.com/wb7p8r1B/heap-does-not-grow-up-to-maxheap) – Pedro Sánchez Terraf Jan 28 '20 at 21:00
  • 1
    I recommend asking such questions on the isabelle-users mailing list as well. The Isabelle maintainers (who are probably the best people to answer this) tend to be much more active there than on StackOverflow. – Manuel Eberl Jan 30 '20 at 08:01

1 Answers1

2

Following the advice by @ManuelEberl, I asked this question in the isabelle-users list, and the point seems to be that the building process used by the PIDE (jEdit) is not as parallel-intensive as that of the isabelle build command. All the information in this answer was provided by M. Wenzel on the list. I quote:

both PIDE and build are using multiple threads by default, but the overall profile of the parallel application comes out quite differently. E.g. in PIDE proofs are only parallel in terminal positions (e.g. by).

You can also try this:

isabelle build -o parallel_proofs=0

I.e. multithreading is enabled, but proofs are not forked.

This seems to be the setting I was looking for.

For those that (like myself) have had a limited exposure to the isabelle tool wrapper, the command

isabelle options -l

will show a full list of options of the whole Isabelle system.

Pedro Sánchez Terraf
  • 231
  • 1
  • 7