Email Gateway (Aug 23 2022 at 09:22): Email Gateway (Aug 23 2022 at 09:22):From: Norbert Schirmer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi,
In the following scenario we get an exception in the case we run the build with 'threads=1’. A higher number of threads let’s the exception disappear.
Test.thy:
theory Test
imports Main
begin
lemma X_1: True by rule
lemma X_2: True by rule
lemmas X = X_1 X_2
end
ROOT:
session Test = HOL +
theories Test
Applications/Isabelle2020.app/Isabelle/bin/isabelle build -v -c -d . -o threads=1 Test
Started at Tue Jul 21 15:29:30 GMT+2 2020 (polyml-5.8.1_x86_64_32-darwin on MacBook-Pro)
ISABELLE_BUILD_OPTIONS=""
ML_PLATFORM="x86_64_32-darwin"
ML_HOME="/Applications/Isabelle2020.app/Contents/Resources/Isabelle2020/contrib/polyml-5.8.1-20200228/x86_64_32-darwin"
ML_SYSTEM="polyml-5.8.1"
ML_OPTIONS="--minheap 500"
Session Pure/Pure
Session Tools/Tools
Session HOL/HOL (main)
Session Unsorted/Test
Cleaned Test
Running Test ...
Test: theory Test.Test
Test FAILED
(see also /Users/schirmer/.isabelle/Isabelle2020/heaps/polyml-5.8.1_x86_64_32-darwin/log/Test)
Loading theory "Test.Test"
*** exception THM 0 raised (line 105 of "global_theory.ML"):
*** Duplicate use of derivation identity for Test.X_1 vs. Test.X(1)
*** True
*** At command "end" (line 7 of "~/Projects/tmp/Test/Test.thy")
Unfinished session(s): Test
Finished at Tue Jul 21 15:29:34 GMT+2 2020
0:00:03 elapsed time
/Applications/Isabelle2020.app/Isabelle/bin/isabelle build -v -c -d . -o threads=2 Test
Started at Tue Jul 21 15:29:38 GMT+2 2020 (polyml-5.8.1_x86_64_32-darwin on MacBook-Pro)
ISABELLE_BUILD_OPTIONS=""
ML_PLATFORM="x86_64_32-darwin"
ML_HOME="/Applications/Isabelle2020.app/Contents/Resources/Isabelle2020/contrib/polyml-5.8.1-20200228/x86_64_32-darwin"
ML_SYSTEM="polyml-5.8.1"
ML_OPTIONS="--minheap 500"
Session Pure/Pure
Session Tools/Tools
Session HOL/HOL (main)
Session Unsorted/Test
Cleaned Test
Running Test ...
Test: theory Test.Test
Timing Test (2 threads, 0.031s elapsed time, 0.049s cpu time, 0.000s GC time, factor 1.57)
Finished Test (0:00:00 elapsed time)
Finished at Tue Jul 21 15:29:42 GMT+2 2020
0:00:03 elapsed time
Regards,
Norbert
Last updated: Apr 25 2024 at 20:15 UTC