Построение сессии с использованием `isabelle` vs jEdit

Question

Я работал в сеансе Isabelle 2019, который стал немного больше, и в какой-то момент я больше не мог его строить, используя isabelle build в моей машине с 8G RAM. Тем не менее, когда я открываю основной файл теории с помощью jEdit (работает isabelle jedit -d .), сессия создается без проблем.

Как настроить процесс сборки так, чтобы он работал так же гладко, как графический интерфейс?

Далее я приведу некоторые подробности.

Основным симптомом является то, что процесс Poly / ML в какой-то момент останавливается; на самом деле это не дает сбоя, но не завершается в течение разумного промежутка времени (~ 20 минут, когда успешная сборка заняла бы 3 'на моем компьютере). "--minheap 5500" было достаточно, чтобы решить эту проблему, но после этого мы решили разделить сессию на две части (код больше не добавлялся, просто изменение в файле ROOT), и после этого дальнейшая корректировка не решила проблему. С другой стороны, машина с оперативной памятью 16G без проблем собирается без каких-либо дополнительных настроек.

EDIT. Я проверил опции, используемые jEdit; эти релевантные (я полагаю) --minheap 500 --gcthreads 0 (последний по умолчанию). Я пытался с этим безуспешно. Я также отметил, что команда build имеет отдельную опцию --eval Command_Line.tool0 (fn () => (Build.build "/tmp/isabelle-pedro/buildNNNNNNNNNNNNN")), где NNNNNNNNNNNNN - некоторые цифры.

Answer 1

Следуя совету @ManuelEberl, я задал этот вопрос в списке isabelle-users , и, похоже, дело в том, что процесс сборки, используемый PIDE (jEdit), не так интенсивно параллелен как команда isabelle build. Вся информация в этом ответе была предоставлена ​​ M. Венцель в списке . Я цитирую:

и PIDE, и build используют по умолчанию несколько потоков, но общий профиль параллельного приложения выглядит совсем по-другому. Например, доказательства PIDE параллельны только в терминалах (например, by).

Вы также можете попробовать это:

isabelle build -o parallel_proofs=0

Т.е. многопоточность включена, но доказательства не разглашаются.

Похоже, что это именно то, что я искал.

Для тех, кто (как и я) имел ограниченную доступность обертки для инструмента isabelle команда

isabelle options -l

покажет полный список опций всей системы Изабель.