Walther Neuper <walther.neuper@jku.at> [Tue, 05 Jan 2021 17:29:39 +0100] rev 60141
step 4.7: cannot fill 2 gaps tracing Outer_Syntax .. Output.report
note: see Greatest_Common_Divisor.thy, subsection ?fill gaps in traces?
Walther Neuper <walther.neuper@jku.at> [Mon, 21 Dec 2020 15:13:49 +0100] rev 60140
step 4.6: two gaps in trace on SPARK
note: no caller found for "Syntax.read_props" and "Proof.have"
Walther Neuper <walther.neuper@jku.at> [Mon, 21 Dec 2020 11:55:10 +0100] rev 60139
step 4.5: separate trace for specific proof element
the proof element is "from ?0 < d?" plus "have "0 ? c mod d""
Walther Neuper <walther.neuper@jku.at> [Thu, 17 Dec 2020 18:00:27 +0100] rev 60138
step 4.4: call hierarchy up from Syntax.check_terms, partially
Walther Neuper <walther.neuper@jku.at> [Thu, 17 Dec 2020 11:45:12 +0100] rev 60137
tuned
Walther Neuper <walther.neuper@jku.at> [Thu, 17 Dec 2020 11:42:18 +0100] rev 60136
step 4.3: parse Problem + Specification; this is inappropriate..
.because Position.T are dropped, so no feedback can be allocated.
Walther Neuper <walther.neuper@jku.at> [Thu, 17 Dec 2020 11:22:53 +0100] rev 60135
cleanup
Walther Neuper <walther.neuper@jku.at> [Thu, 17 Dec 2020 09:10:30 +0100] rev 60134
step 4.2: writeln at calling Output.report uncover some of proof handling
Walther Neuper <walther.neuper@jku.at> [Wed, 16 Dec 2020 16:25:55 +0100] rev 60133
step 4.1: @{print} at calling Output.report fails
..because no call of Output.report is reached by spark_vc procedure_g_c_d_4,
while in Naproche all semantic annotations are done by ONE Output.report .
Walther Neuper <walther.neuper@jku.at> [Tue, 15 Dec 2020 15:10:38 +0100] rev 60132
step 4: use Naproche as a model for checking input
note: ParseC.problem (without "Problem") replaced ParseC.problem_headline