Email Gateway (Apr 28 2021 at 17:08): Email Gateway (Apr 28 2021 at 17:08):From: Alex Meyer <alex153@outlook.lv>
I tried to keep QRHL_Operations.thy in place but commented all the content out:
theory QRHL_Operations
imports Main
(* QRHL_Core Tactics Joint_Measure Extended_Sorry
Weakest_Precondition Joint_Sample Squash_Sampling O2H Semi_Classical_Search *)
begin
(*
ML_file "qrhl_operations.ML"
*)
end
Currently this allowes me to proceed with building the workspace and without loading QRHL-related theories. So, maybe I will managed to ignite my proof process.
Alex
No: Alex Meyer <alex153@outlook.lv>
Nosūtīts: trešdiena, 2021. gada 28. aprīlis 17:41
Kam: Alex Meyer <alex153@outlook.lv>
Tēma: Is it possible to use QRHL tool without reference to QRHL theories?
Hi!
I am not sure if this is the appropriate avanue to ask about QRHL tool, but possibly is - because this interface seems to be quite handy and general.
I am trying to use TopLevel etc. infrastructure from QRHL tool for issuing theory commands (e.g. tactics) and for reading back the generated open goals and their content (which I can parse using my own code and scala-isabelle).
But I have my own simple theory file and I don't want to import QRHL theories (they are in active developemnt), but after some trial-and-error efforts I have came up with the followint ROOTS content:
chapter Algo
session QRHL = Pure +
description "
Classical Higher-order Logic.
"
document_files
"Max_Of_Two_Integers_Real"
session "QRHL-Scala" in "fake-session-dir/6" = QRHL +
sessions QRHL
theories QRHL.Scalasrc/Pure
It seems to me that the session with name QRHL is required abd that there should be parent session QRHL-Scala. Otherwise there are errors like
Last updated: Jul 15 2022 at 23:21 UTC