Stream: General

Topic: Efficient session loading from AFP

Tobias Rothmann (Jun 23 2023 at 13:34):

Hi,
I'm importing theories from the AFP, which have an extensive background, and Isabelle is taking forever to check the background theories. To come to my question; is there a way one can get around this whole background checking of AFP theories, so Isabelle only checks my working session/directory?
I built my own session (i.e. ROOT-file), which looks like this:

session "KZG"  = "CryptHOL" +
  options [timeout = 600]
  sessions
    "CRYSTALS-Kyber"
    "Sigma_Commit_Crypto"
    "Berlekamp_Zassenhaus"

However, from my understanding, a session can only have one parent session (which doesn't have to be checked) and the other sessions still need to be checked (which still takes a lot of time).
Help is greatly appreciated!

Mathias Fleury (Jun 23 2023 at 13:57):

The old wisdom was to create a session with all imports, but nowadays it is sufficient to specify the session to act as parent:

isabelle jedit -R KZG

Tobias Rothmann (Jun 23 2023 at 14:26):

Thanks for the response first of all.
I am already using the session, so my problem is more "how can I 'have' multiple parent sessions"/ a way to get around checking all other sessions (i.e. CRYSTALS, Sigma_Commit and BKZ) that are not parent (as only one session can be a parent and thus doesn't need to be checked by Isabelle (from my understanding)).
I think what you're proposing is just a way to use the session I already built and use, right?

Mathias Fleury (Jun 23 2023 at 14:31):

Yes, but the very thing Isabelle/jEdit does is compiling the parent and all the imported sessions…

Mathias Fleury (Jun 23 2023 at 14:33):

This is what happens when I start one of my session:

Build started for Isabelle/Watched_Literals_requirements(Isabelle_LLVM) ...
Building Watched_Literals_requirements(Isabelle_LLVM) ...
Watched_Literals_requirements(Isabelle_LLVM): theory HOL-Library.Multiset_Order
Watched_Literals_requirements(Isabelle_LLVM): theory Weidenbach_Book_Base.Explorer
Watched_Literals_requirements(Isabelle_LLVM): theory Nested_Multisets_Ordinals.Multiset_More
Watched_Literals_requirements(Isabelle_LLVM): theory Ordered_Resolution_Prover.Clausal_Logic
Watched_Literals_requirements(Isabelle_LLVM): theory CDCL.CDCL_WNOT_Measure
Watched_Literals_requirements(Isabelle_LLVM): theory Entailment_Definition.Partial_Herbrand_Interpretation

See how many session I use?

Mathias Fleury (Jun 23 2023 at 14:35):

They all get imported and they do not get recompiled when I restart Isa/jEdit

Tobias Rothmann (Jun 23 2023 at 17:08):

Do you mind sharing your build command? My build-log looks a bit different, which is probably the problem.
As for me, it needs to load theories from within the sessions it clearly contains, even after multiple restarts and rebuilds.
(see here:)
image.png
image.png

Mathias Fleury (Jun 23 2023 at 17:23):

My stuff is here: https://bitbucket.org/isafol/isafol/src/master/Weidenbach_Book/Watched_Literals/ROOT

Mathias Fleury (Jun 23 2023 at 17:24):

is your development somewhere?

Mathias Fleury (Jun 23 2023 at 17:35):

okay there is something going on here, which I avoid because I have mostly linear stuff

Tobias Rothmann (Jun 23 2023 at 18:00):

Thanks for sharing!
My development is not public yet as it is a university project.
By build command, I meant a command in the sense "isabelle build [OPTIONS] [SESSIONS ...]", would be greatly appreciated :)

Mathias Fleury (Jun 23 2023 at 18:06):

I am trying but I failed so far :(

Tobias Rothmann (Jun 23 2023 at 18:21):

Ah I see, thanks a lot for your help! :)

Mathias Fleury (Jun 23 2023 at 20:02):

I tried the old trick to have an intermediate session with all imports but that failed

Wolfgang Jeltsch (Jun 23 2023 at 20:16):

My development is not public yet as it is a university project.

What? In the good old days, you would have said, “My development is surely public, as it is a university project”.

Mathias Fleury (Jun 24 2023 at 05:22):

University have more and more gitlab/github/... stuff that cannot be reached without account

Mathias Fleury (Jun 24 2023 at 05:22):

(the isafol repo predates that actually)

Mathias Fleury (Jun 24 2023 at 08:09):

Found it!

Mathias Fleury (Jun 24 2023 at 08:09):

And this people is way you should always put ALL theories in the ROOT file

Mathias Fleury (Jun 24 2023 at 08:12):

Isabelle only precompiles theories that are imported in a theory that is listed in the theories section of the ROOT

Mathias Fleury (Jun 24 2023 at 08:13):

Tested with:

chapter KZG

session "KZG" (KZG)  = "CryptHOL" +
  description ‹Test›
  options [timeout = 600]
  sessions
    "CRYSTALS-Kyber"
    "Sigma_Commit_Crypto"
    "Berlekamp_Zassenhaus"
  theories
    Test

theory Test
  imports Berlekamp_Zassenhaus.Poly_Mod
    "CRYSTALS-Kyber.Kyber_spec"
begin

end

Mathias Fleury (Jun 24 2023 at 08:13):

Then the very normal isabelle build will do the right thing

Tobias Rothmann (Jun 24 2023 at 10:11):

Ah yes, that makes perfect sense. Tried it out and worked perfectly. Thanks a lot for your help! Although the solution seems simple I've been struggling a lot with the ROOT/Session system, so greatly appreciate you're effort and, again, thanks a lot!

Mathias Fleury (Jun 24 2023 at 11:04):

Now the hard part: I should remember it for the next question :laughing:

Last updated: May 02 2024 at 04:18 UTC