Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle build failure for ’threads=1’


view this post on Zulip Email Gateway (Jul 22 2020 at 06:26):

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="

view this post on Zulip Email Gateway (Aug 05 2020 at 09:50):

From: Makarius <makarius@sketis.net>
These are corner cases in the internal naming of derivations (proof terms) and
the fact name space.

You should generally avoid fact names like X_1, X_2, because the system likes
to use that form to generate an internal name for the individual parts of the
multi-fact X.

Generally note that a more standard format for indexed names is X1 or X⇩1.

Makarius


Last updated: Jul 15 2022 at 23:21 UTC