Email Gateway (Feb 18 2022 at 01:36): Email Gateway (Feb 18 2022 at 01:36):From: Peyman Derafsh Kavian <peymankavian@gmail.com>
Hello Isabelle team,
I recently contacted you regarding an issue running HOL-TestGen tool. You
advised me to run the tool on Linux. I could migrate the tool to isabelle
2021 on Linux but when I try to run the tool, I get the error below. Could
you please advise?
[peyman@localhost hol-testgen-1.9.1]$
~/Isabelle-linux/Isabelle2021-1/bin/isabelle build -d . -b HOL-TestGen
Building HOL-TestGenLib ...
HOL-TestGenLib FAILED
(see also
/home/peyman/.isabelle/Isabelle2021-1/heaps/polyml-5.9_x86_64_32-linux/log/HOL-TestGenLib)
*** Inner syntax error (line 477 of "~/Hol test
gen/hol-testgen-1.9.1/src/test/Monads.thy")
*** at "* fail - strict * ) | Some ( outs , σ'' ) ⇒ Some ( out # outs , σ''
) )
*** )"
*** Failed to parse prop
*** At command "fun" (line 471 of "~/Hol test
gen/hol-testgen-1.9.1/src/test/Monads.thy")
*** Failed to load theory "HOL-TestGenLib.EFSM_Toolkit" (unresolved
"HOL-TestGenLib.Monads")
*** Failed to load theory "HOL-TestGenLib.Observers" (unresolved
"HOL-TestGenLib.Monads")
*** Failed to load theory "HOL-TestGenLib.TestRefinements" (unresolved
"HOL-TestGenLib.Monads")
*** Failed to load theory "HOL-TestGenLib.TestLib" (unresolved
"HOL-TestGenLib.EFSM_Toolkit", "HOL-TestGenLib.Monads",
"HOL-TestGenLib.Observers", "HOL-TestGenLib.TestRefinements")
HOL-TestGen CANCELLED
Unfinished session(s): HOL-TestGen, HOL-TestGenLib
0:00:49 elapsed time, 0:00:33 cpu time, factor 0.67
Regards,
Peyman Derafshkavian
Concordia university Montreal, Canada
Last updated: Jul 15 2022 at 23:21 UTC