Walther Neuper <wneuper@ist.tugraz.at> [Tue, 05 Jan 2016 11:13:20 +0100] rev 59199
experiments with ROOT/paths in libisabelle-procol
# Note: on the java-side in ~/proto4/libisabelle running
libisabelle$ ./sbt
> appBootstrap/run --version 2015
# gives the error
ERROR(Bad parent session "../isabelle-common/HOL-Codec" for "HOL-Protocol2015"...
Walther Neuper <wneuper@ist.tugraz.at> [Mon, 04 Jan 2016 13:10:23 +0100] rev 59198
libisabelle/Protocol: all subsequent operation_setup compile without error
Note the difference between 1st operation_setup an the subsequent:
Coding the 2nd analogously to the 1st gives the (reasonable)
ML error:
Type error in function application. Function: Protocol.add_operation "autocalculate" : ('a, 'b) Protocol.operation -> Protocol.flags -> unit
Argument: ((fn intree => (let val ... = ...; val ...; ... in result end) handle ERROR msg => ... ... msg)) : XML.tree -> XML.tree
Reason: Can't unify {action: 'a -> 'b, from_lib: 'a codec, to_lib: 'b codec} to XML.tree -> XML.tree (Incompatible types)
Walther Neuper <wneuper@ist.tugraz.at> [Mon, 04 Jan 2016 12:32:01 +0100] rev 59197
libisabelle/Protocol: 1st operation_setup compiles without error
manually merged in
https://github.com/larsrh/libisabelle-protocol/commit/4b82f568900aeb9445abadf6d0d9647f68fed39e
Walther Neuper <wneuper@ist.tugraz.at> [Mon, 21 Dec 2015 14:19:03 +0100] rev 59196
Isabelle2014-->15: Test_Isac is perfect
For "sqrt (-1)" compare dd627569647c.
Walther Neuper <wneuper@ist.tugraz.at> [Mon, 21 Dec 2015 14:06:19 +0100] rev 59195
Isabelle2014-->15: finished closed Thm.thy for tests
Walther Neuper <wneuper@ist.tugraz.at> [Mon, 21 Dec 2015 13:58:02 +0100] rev 59194
Isabelle2014-->2015: dropped tests not required any more
Walther Neuper <wneuper@ist.tugraz.at> [Mon, 21 Dec 2015 13:35:41 +0100] rev 59193
built session Isac without libisabelle Protocol
Walther Neuper <wneuper@ist.tugraz.at> [Thu, 17 Dec 2015 15:48:13 +0100] rev 59192
added libisabelle-protocol
cloned from
https://github.com/larsrh/libisabelle-protocol/commit/c33db5fef8af6548c494705e55e6b56e976a10a9
and copied here without .git* and without isabelle-2014
Walther Neuper <wneuper@ist.tugraz.at> [Thu, 17 Dec 2015 15:46:49 +0100] rev 59191
Build_Isac works with Isabelle2015, excludes Protocol.thy
Walther Neuper <wneuper@ist.tugraz.at> [Mon, 07 Dec 2015 16:07:24 +0100] rev 59190
Isabelle2014-->15: removed errors from d9c3e373f8f5
Note: Protocol.thy is the only source of errors now.