Email Gateway (Mar 08 2021 at 13:36): Email Gateway (Mar 08 2021 at 13:36):From: Walther Neuper <walther.neuper@jku.at>
the update of working code from Isabelle2020 to 21 shows that "::
thy_load" has changed and now takes a kind of constant, for instance
spark_siv, instead of strings.
we use SPARK as a model for our application, but are not yet successful
with the following adaption of our code ...
/----------- *.thy ------------------------------------
keywords "Example" :: thy_load (isac_example)
val _ =
Outer_Syntax.command \<^command_keyword>‹Example›
"start a Calculation from a Formalise-file"
(Resources.provide_parse_files (Command_Span.extensions ["str"]) -- Parse.parname
>> (Toplevel.theory o (Preliminary.load_formalisation ParseC.formalise)));
\---------- *.thy ------------------------------------
/----------- isac.scala ------------------------------
package isabelle.isac
import isabelle._
object ISAC
{ class Load_Command1 extends Command_Span.Load_Command("isac_example")
{ override val extensions: List[String] = List("str") }
}
\---------- isac.scala ------------------------------
... because keywords "Example" raises the error
Unknown load command specification: "isac_example"
... which is no surprise. However taking the model
keywords "spark_open" :: thy_load (spark_siv)
... and looking for the definition of spark_siv, there are only two
occurrences of spark_siv
~$ grep -r spark_siv src/HOL/SPARK/
src/HOL/SPARK/SPARK_Setup.thy: and "spark_open" :: thy_load (spark_siv)
src/HOL/SPARK/Tools/spark.scala: class Load_Command2 extends Command_Span.Load_Command("spark_siv")
... so the question: where / how is the constant spark_siv defined ?
Any hint is welcome,
Walther
Email Gateway (Mar 08 2021 at 18:56):From: Makarius <makarius@sketis.net>
You need to declare your add-ons to Isabelle/Scala formally via
isabelle_scala_service in etc/settings, e.g. see
https://isabelle.sketis.net/repos/isabelle-release/file/Isabelle2021/src/HOL/SPARK/etc/settings
BTW, this is how I figured out the internal class name, e.g. in "isabelle scala":
classOf[isabelle.spark.SPARK.Load_Command1].getName
An alternative is to ignore the whole thing and merely use literal file names
with explicit extension. E.g. see my change to 'boogie_file' for Isabelle2021:
https://isabelle.sketis.net/repos/isabelle-release/rev/b808eddc83cf
Makarius
Email Gateway (Mar 10 2021 at 17:22):From: Walther Neuper <walther.neuper@jku.at>
Thank you for the hints. I also added also the two lines "+" ..
src/Pure/Tools/scala_project.scala
"src/HOL/SPARK/Tools" -> Path.explode("isabelle.spark"),
+ "src/Tools/isac/etc" -> Path.explode("isabelle.isac"),
src/Pure/build-jars
declare -a SOURCES=(
src/HOL/SPARK/Tools/spark.scala
+ src/Tools/isac/etc/isac.scala
.. but although Pure was involved in editing, the command
./bin/isabelle jedit ...
did NOT re-build Pure --- how is this achieved most conveniently now,
when Scala is involved?
Many thanks in advance,
Walther
Email Gateway (Mar 10 2021 at 17:33):From: Makarius <makarius@sketis.net>
You should not edit Isabelle/Pure sources in such an adhoc manner.
In Isabelle2021 there is now a complete example application with user-defined
ML and Scala modules, see $NAPROCHE_HOME/Intro.thy in the documentation panel.
The last section of the file has live links to relevant parts of the sources.
In particular, see Admin_Tools/naproche_build for how to build the add-on
Scala module.
For developing the Scala part with IntelliJ IDEA, I use regular "isabelle
scala_project" with some manual symlinks in the generated Gradle project.
The structure of that is rather simple, which is the reason why I've chosen
Gradle to do this.
Makarius
Email Gateway (Mar 12 2021 at 16:17):From: Walther Neuper <walther.neuper@jku.at>
On 08.03.21 19:56, Makarius wrote:
On 08/03/2021 14:35, Walther Neuper wrote:
... so the question: where / how is the constant spark_siv defined ?
You need to declare your add-ons to Isabelle/Scala formally via
isabelle_scala_service in etc/settings, e.g. see
https://isabelle.sketis.net/repos/isabelle-release/file/Isabelle2021/src/HOL/SPARK/etc/settings
in a phase of development where we want to make a test example running
with least effort the following solution appears preferable:
An alternative is to ignore the whole thing and merely use literal file names
with explicit extension. E.g. see my change to 'boogie_file' for Isabelle2021:
https://isabelle.sketis.net/repos/isabelle-release/rev/b808eddc83cf
Thus we have (in Calculation.thy):
keywords "Example" :: thy_load
and
Example ‹/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70.str›
which nicely evaluates related code in Calculation.thy. However, we need
to create a session
./bin/isabelle build -v -b Isac
which causes the error message (see "*.str.str" ..)
Isac FAILED
(see also /home/wneuper/.isabelle/isabisac/heaps/polyml-5.8.2_x86_64_32-linux/log/Isac)
*** Failed to load theory "Isac.BridgeJEdit" (unresolved "Isac.Calculation")
*** Failed to load theory "Isac.Build_Isac" (unresolved "Isac.BridgeJEdit")
*** No such file: "/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70.str.str" (line 230 of "~~/src/Tools/isac/BridgeJEdit/Calculation.thy")
*** At command "Example" (line 230 of "~~/src/Tools/isac/BridgeJEdit/Calculation.thy")
Unfinished session(s): Isac
Studying ~~/src/HOL/ROOT we found "dokument_files" (would require
/document/) and "export_files", but here we would need something like
"import_files".
Is here a simple way out or should we go the long way via IntelliJ Idea?
Walther
Email Gateway (Mar 12 2021 at 16:28):From: Makarius <makarius@sketis.net>
On 12/03/2021 17:17, Walther Neuper wrote:
Thus we have (in Calculation.thy):
keywords "Example" :: thy_load
and
Example ‹/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70.str›
which nicely evaluates related code in Calculation.thy. However, we need to
create a session./bin/isabelle build -v -b Isac
which causes the error message (see "*.str.str" ..)
Isac FAILED
(see also /home/wneuper/.isabelle/isabisac/heaps/polyml-5.8.2_x86_64_32-linux/log/Isac)
*** Failed to load theory "Isac.BridgeJEdit" (unresolved "Isac.Calculation")
*** Failed to load theory "Isac.Build_Isac" (unresolved "Isac.BridgeJEdit")
*** No such file: "/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70.str.str" (line 230 of "~~/src/Tools/isac/BridgeJEdit/Calculation.thy")
*** At command "Example" (line 230 of "~~/src/Tools/isac/BridgeJEdit/Calculation.thy")
Unfinished session(s): Isac
The error appears to stem from your Isabelle/ML implementation of the command:
it probably still adds another file extension.
Studying ~~/src/HOL/ROOT we found "dokument_files" (would require
/document/) and "export_files", but here we would need something like
"import_files".
Such declarations of imported files were required many years ago. Today we
have everything in "theory keywords ... :: thy_load" and "isabelle build"
picks the information from there.
Is here a simple way out or should we go the long way via IntelliJ Idea?
For Isabelle/ML problems you merely require Isabelle/jEdit as IDE.
Makarius
Last updated: Jan 04 2025 at 20:18 UTC