Email Gateway (Apr 28 2021 at 16:35): Email Gateway (Apr 28 2021 at 16:35):From: Alex Meyer <alex153@outlook.lv>
Hi!
I am not sure if this is the appropriate venue to ask about QRHL tool, but possibly it 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 developement, e.g. there is no published code for Jordan_Normal_Form and for Banach_Steinhaus). After some trial-and-error efforts I have came up with the followint ROOT content:
chapter Algo
session QRHL = Pure +
description "
Classical Higher-order Logic.
"
document_files
"Max_Of_Two_Integers_Real"
So, there are no references to QRH (especially - not for Extra theories).
Is it OK that QRHL tool asks me to provide theories for those QRHL extra theories? Is the integration to QRHL so tight? I have error messages:
*** Building Isabelle (may take a while, especially the first time, e.g., 20-60min)...
Exception in thread "main" qrhl.UserException: (in Isabelle) No such file: "/cygdrive/c/Workspace-IntelliJ/qrhl-tool/Conjugate.thy"
The error(s) above occurred for theory "Jordan_Normal_Form.Conjugate" (line 3 of "/cygdrive/c/Workspace-IntelliJ/qrhl-tool/Extra_Infinite_Set_Sum.thy")
(required by "QRHL.QRHL_Operations" via "QRHL.QRHL_Core" via "QRHL.BOLegacy" via "Tensor_Product.Tensor_Product_Code" via "Tensor_Product.Tensor_Product" via "Bounded_Operators.Complex_L2" via "Bounded_Operators-Extra.Extra_Infinite_Set_Sum")
at qrhl.UserException$.apply(State.scala:50)
And another thing. My qrhl-tool.conf file is:
isabelle-home = C:\Homes\Isabelle2020\Isabelle2020
My project directory for the qrhl-tool is:
C:\Workspace-IntelliJ\qrhl-tool
And - as one can see from the error message - Isabelle is seeking theories in the C:\Workspace-IntelliJ\qrhl-tool directory and not in its own source directories (C:\Homes\Isabelle2020\Isabelle2020\src). Temporary solution is to copy thy files manually when some file is required by the build error message, but when QRHL specific theories are involved then this copying is too much.
Thanks in advance!
Alex
Last updated: Jul 15 2022 at 23:21 UTC