Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Repo info
Activity
    Lukas Stevens
    @lukasstevens
    Hi, I saw your post on the mailing list about the scala-isabelle library. I am currently trying to get a student to develop a linter for Isabelle. The main problem (I suspect) is that PIDE is not documented and the barrier of entry is high. Could scala-isabelle be extended to load theories and read theory markup?
    Dominique Unruh
    @dominique-unruh
    Loading theories as one file is easy (i.e., there are functions for that in the library already).
    I have also done the following (in separate experiments): Loading a theory, splitting it into commands, and applying each command separately, to get the theory in the end. (Allows to inspect the state in between or even to operate on the state from the Scala side between operations.)
    What I have not done so far, is parsing a theory and accessing the "reporting", i.e., the meta-data that is sent to the IDE that says, e.g., which substring is a variable, where control-click should jump to, etc. Here the question is probably less a question of scala-isabelle's capabilities, but of finding out what the corresponding operations in Isabelle/ML are.
    Is the latter what you mean by "read theory markup"?
    Dominique Unruh
    @dominique-unruh
    @lukasstevens (Because I don't know if gitter provides notifications otherwise.)
    Lukas Stevens
    @lukasstevens
    Yes the latter is what I mean
    However, I have to say that you shouldn't invest too much time since the linter should probably be integrated into the isabelle distribution at some point and I don't know if Makarius or you would be in favor of pulling scala-isabelle into the distribution.
    As an example: the linter should detect usages of sorry
    Dominique Unruh
    @dominique-unruh
    I had a look, it looks it shouldn't be too hard to get the "reporting". There is a global mutable reference in Isabelle where one can install a function that is called with all those kinds of messages. It would be easy to add (via a scala-isabelle call) a function there that logs all those messages in a global list, and then read from that list from scala-isabelle. (I don't like the fact that this mutates a global state, but there is no real problem with that in this setting.) That list would then consist of XML fragments providing the reporting for Isabelle theories.
    But you are probably right, Makarius might push towards a PIDE solution if the linter is to be integrated in Isabelle/jedit, for example.
    Dominique Unruh
    @dominique-unruh

    As an example: the linter should detect usages of sorry

    This specific thing can already be achieved using the command "thm_oracles" (new in Isabelle 2020). But that's a special case because that information is logged in the theorems.

    If your planned linter is simply going to produce a report, an alternative might also be to directly implement it inside Isabelle. I.e., you would define an Isabelle command "linter blabla" which would then lint the theory or theorem bla by looking at the reporting that was produced when parsing bla. That linter could then output the report in the output window, with clickable position markers to jump to the mentioned positions in the code. And the linter could get the reporting information by adding a hook into the "Private_Output.report_fn" (I think that was the name) when the linter theory is loaded.
    So let me know – if you decide to try it with scala-isabelle, I can add the missing bits and pieces. But otherwise I won't. :)
    Albert Jiang
    @albertqjiang

    Hi Dominique, thanks for answering my question related to translating Isar commands on the Isabelle mailing list. I've been trying to run the file but always encounter some problems related to java/scala/sbt versions. I wonder if you can share your setup of these configurations and commands to run the file?

    I'm also working to figure out how to use the tools in ExecuteIsar to run a translation of a minimal proof in Isar. Is it right to think I would only need to substitute the text from line 88 with my own theory string? Thank you!

    Dominique Unruh
    @dominique-unruh

    I just tried to run it with sbt 1.3.13, Java 14, Scala 2.13. (But it should work with other configurations, too.) To run it, I checked out the master branch of the git repo of scala-isabelle (but I also tried with the v0.3.0 tag), and ran

    sbt 'test:runMain de.unruh.isabelle.experiments.ExecuteIsar'

    (This should select the right Scala and sbt version automatically, but will use whichever Java you get when running java -version)

    Of course, running it from the command line is not really convenient, but it should be the most reproducible way for finding out what doesn't work. Usually, I work with Intelli/J IDEA.
    And yes, you can put any theory in the string theorySource. Only caveat: it will not find theories that are not in the HOL image without extra steps. But I guess that's for the next step. :) (There is a command to register theory directories.)
    Btw, see the file IsabelleTest.scala, variable isabelleHome to set the path where Isabelle is loaded since the experiment file just uses the config from there.
    Albert Jiang
    @albertqjiang
    Thank you Dominique! This is a great help! I managed to run the experiment.
    Dominique Unruh
    @dominique-unruh
    Excellent. It should also be possible to run it in Intelli/J if you just open the .sbt as a project and then go to the main-method of the experiment and press Ctrl-Shift-F10.
    Dominique Unruh
    @dominique-unruh
    By the way, the things involving the ScalaKeywords theory, the ScalaTransition class, and the "scala" Isabelle command you can probably just ignore/remove. They are some extra experiments beyond just executing a theory.
    Albert Jiang
    @albertqjiang
    Hi Dominique, I've been working on this small project https://github.com/albertqjiang/PISA that uses the scala-isabelle library. Its main purpose is to provide a gym-like environment in python suitable for downstream machine learning developments. I have adapted the code of yours in https://github.com/dominique-unruh/scala-isabelle/tree/master/src/test/scala/de/unruh/isabelle/experiments to the code in https://github.com/albertqjiang/PISA/tree/main/src/main/scala/pisa, with clear references to your experiment code. Thank you very much for your help along the way and you can include this as a project that uses scala-isabelle if you like. Let me know if you have any suggestions!
    Dominique Unruh
    @dominique-unruh
    @albertqjiang Since I don't know gym (besides what I Googled right now), I don't understand how PISA is used or what it is for. Maybe you can tell me a one-line description (like "qrhl-tool – A theorem prover for post-quantum security.") for including in the list of projects? But I'm curious what PISA is for: it is for testing ML algorithms implemented in Isabelle, or for running ML algorithms that train to use Isabelle, or something else?
    Albert Jiang
    @albertqjiang
    @dominique-unruh Gladly! PISA - A reinforcement learning environment for theorem proving in Isabelle. A slightly longer version: PISA is for running ML (RL specifically) algorithms written in Python that write proofs with Isabelle. It provides a Markov Decision Process for ML algorithms to operate in.
    Since I have very green hands when it comes to open-source development and scala, please kindly let me know if there are improper things (e.g. not strong enough references to your experiment code etc.) Thank you!
    Dominique Unruh
    @dominique-unruh
    Concerning the references to my code: I myself am not an expert as to what is formally the right thing to do, but personally I am satisfied with this reference.
    @albertqjiang I have added a link to PISA to the readme. (https://github.com/dominique-unruh/scala-isabelle)
    Albert Jiang
    @albertqjiang
    Sorry for the very late reply. Thank you, Dominique, for including PISA in the list of projects using scala-isabelle. That is very cool.
    Albert Jiang
    @albertqjiang

    Hi Dominique, I have a technical question regarding using scala-isabelle and would appreciate it a lot if you could give some suggestions.

    I've been trying to use scala-isabelle to read theory files from the archive of formal proofs and execute them segment by segment. Please see the example here. It works when the theory file imports things like Main and Complex_Main that are in the heap, but fails when it's using things defined in custom-defined .thy files. In the example I tried to read from afp/thys/Functional-Automata/Automata.thy and use toplevel to execute the first sentence "theory Automata imports DA NAe begin".

    I then got the following error in the screenshot. Isabelle cannot find the theory DA. I suspect that this is a problem with the Isabelle and TheoryManager setup and workingDirectory but cannot figure out the problem with the example given above. If you have spare time, could you please point out where my mistake was? Or better still, can you show me how one would generally execute statements such as "theory Automata imports DA NAe begin" that imports theories from afp? Many many thank!

    Screenshot 2021-02-19 at 17.54.10.png
    Albert Jiang
    @albertqjiang
    Nevermind. The issue is solved.
    Dominique Unruh
    @dominique-unruh

    @albertqjiang Glad that it is solved. Just in case my take on it: Unfortunately, Isabelle itself does not know the paths in which different sessions are found. (The ROOT/ROOTS files are not parsed by Isabelle ML process itself but by the Scala-programs that invoke it. This makes them inaccessible in the scala-isabelle context.) But one can manually register session directories in scala-isabelle:

    See Theory(String) and Theory.registerSessionDirectoriesNow for more information.

    https://javadoc.io/static/de.unruh/scala-isabelle_2.13/0.3.0/de/unruh/isabelle/pure/Theory$.html#registerSessionDirectoriesNow(paths:(String,java.nio.file.Path)*)(implicitisabelle:de.unruh.isabelle.control.Isabelle,implicitec:scala.concurrent.ExecutionContext):Unit

    https://javadoc.io/static/de.unruh/scala-isabelle_2.13/0.3.0/de/unruh/isabelle/pure/Theory$.html#apply(name:String)(implicitisabelle:de.unruh.isabelle.control.Isabelle,implicitec:scala.concurrent.ExecutionContext):de.unruh.isabelle.pure.Theory

    Albert Jiang
    @albertqjiang
    Thank you, Dominique!!! @dominique-unruh
    Albert Jiang
    @albertqjiang
    Hi Dominique, is there a way of loading custom theories from their built heap images? e.g. I built some project from afp and it has a heap image stored at $USERHOME/.isabelle/Isabelle2020/heaps/polyml-5.8.1_x86_64_32-darwin/Functional-Automata. Can I directly load theories from it with "Theory(Functional-Automata.RegExp2NA)" so they don't have to be built again? I tried a few times with scala-isabelle with setup.userDir = $USERHOME/.isabelle. It doesn't seem to search for heap images and returns errors 'de.unruh.isabelle.control.IsabelleException: No such file: "$USERHOME/.isabelle/RegExp2NA.thy"'. I wonder if this is due to me not doing it right or a possible bug? @dominique-unruh
    18 replies