Walther Neuper <neuper@ist.tugraz.at> [Thu, 26 Sep 2013 14:52:23 +0200] rev 52135
[-Build_Isac] Unsynchronized.ref require specific techniques of investigation
comparison of the two files doc-isac/mlehnfeld/master/ordered-* shows
differences in "eval_rls".
One reason could be that there are two "val eval_rls = ...". For respective
search "./bin/isabelle jedit -l HOL src/Tools/isac/Knowledge/DiffApp.thy &" was used.
The three occurrences of "BEFORE EVALUATING ..." demonstrate the typical,
unhandy behaviour of "val ruleset' = Unsynchronized.ref ...", in this case
accessed by "fun assoc_rls".
Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at> [Wed, 25 Sep 2013 13:52:54 +0100] rev 52134
installation dependent files restored.
Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at> [Wed, 25 Sep 2013 13:33:46 +0100] rev 52133
merged
Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at> [Mon, 23 Sep 2013 22:36:46 +0100] rev 52132
merged
Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at> [Sun, 22 Sep 2013 15:04:27 +0100] rev 52131
.hgignore tuned
Frontend.thy tuned
test_appendFormula added
Walther Neuper <neuper@ist.tugraz.at> [Tue, 24 Sep 2013 11:18:56 +0200] rev 52130
add overlooked Theory_Data
Walther Neuper <neuper@ist.tugraz.at> [Tue, 24 Sep 2013 08:34:01 +0200] rev 52129
values in "val ruleset' = Unsynchronized.ref ..." are non-deterministic..
..non-deterministic due to futures in the parallel evaluation of the
theories dependency graph.
This Unsynchronized.ref and others stem from the original mathematics-engine,
fixed in design under Isabelle2002, where no parallelism was existent.
After focus of Isac's development on the Java front-end, development on
the mathematics-engine was resumed on Isabelle2009. Since then these
Unsynchronized.ref more and more conflicted with parallelism, and thus
are replaced by Theory_Data within these weeks/months.
Walther Neuper <neuper@ist.tugraz.at> [Sun, 22 Sep 2013 18:41:15 +0200] rev 52128
check differences between Theory_Data and "ruleset' = Unsynchronized.ref"
It is worth the effort to study the differences between ruleset' and
KEStore_Elems.get_rls. Some are due to Isabelle's parallel evaluation
of theories, some might cause problems in the next step.
The files ordered-KEStore_Elems.get_rlss and ordered-ruleset.Unsynchronized
are copied from the output in ~/.isabelle/heaps/../log/Isac.gz.
For comparing them a diff-tool is advisable.
Walther Neuper <neuper@ist.tugraz.at> [Sun, 22 Sep 2013 18:29:15 +0200] rev 52127
error in last changeset removed
Walther Neuper <neuper@ist.tugraz.at> [Sun, 22 Sep 2013 18:17:25 +0200] rev 52126
narrow behaviour of Theory_Data and "ruleset' = Unsynchronized.ref"
In order to have KEStore_Elems as similar to the old Unsynchronized.ref,
"fun rls_eq" and future relatives require specific attention.