Minh D (Apr 15 2024 at 03:19): Minh D (Apr 15 2024 at 03:19):I wonder if there is a way to check a proof without needing to open jEdit (using other Isabelle tool than isabelle jedit). I have been trying to use "isabelle process -T Theory" but somehow it does not work if the theory needs some import or include the usage of the "smt" method.
Yong Kiam (Apr 15 2024 at 05:04):maybe isabelle build -D . (this may need your ROOT file to be set up correctly)
Minh D (Apr 23 2024 at 13:11):Yong Kiam said:
maybe
isabelle build -D .(this may need your ROOT file to be set up correctly)
Hi, thank you for the suggestion. I got to work when the "sessions" part in the ROOT file only contains HOL, HOL-Library,.. etc. But what should I do when the "sessions" part also refer to other sessions that are not HOL, HOL-Library,... ?
Mathias Fleury (Apr 23 2024 at 13:14):depends how you installed the external libraries
Mathias Fleury (Apr 23 2024 at 13:15):isabelle build -d some_path -d some_other_path -D .
Minh D (Apr 23 2024 at 13:28):Thank you, I wonder if there is a way to automatically get all the prerequisite sessions, as every time a prerequisite is not included, there appears to be a "Bad import session" error with the build command
Mathias Fleury (Apr 23 2024 at 13:30):I do not know if mk_root https://isabelle.in.tum.de/library/Doc/System/Presentation.html is able to guess the right instantiations
Mathias Fleury (Apr 23 2024 at 13:31):But in any case, looking at the imports should be sufficient to find which ones you need…
Minh D (Apr 23 2024 at 13:33):What if there is a "multi-level" dependency, eg theory C imports theory B, and theory B imports theory A, would there be a way to add -d path/to/theoryA without trial-and-error?
Mathias Fleury (Apr 23 2024 at 13:36):I do not think that you need the transitive ones.
Minh D (Apr 23 2024 at 14:14):Thank you, I tried this with an AFP entry that require multiple levels of dependency, where the import dependency is C -> B -> A, but it showed "Bad theory import", is there a way to do it without having to know the dependency relation B -> A , or having to build the logic image for B?
Mathias Fleury (Apr 23 2024 at 14:18):which one?
Minh D (Apr 23 2024 at 14:22):I tried the Winding_Number_Eval, which depends on Sturm_Tarski and Budan_Fourier, and tried
isabelle build -d path/to/Sturm_Tarski -d path/to/Budan_Fourier -D .
But there was still a message "Bad imports session "Polynomial_Interpolation" for "Sturm_Tarski" (line 3 of path/to/ROOT)
Mathias Fleury (Apr 23 2024 at 14:23):isabelle build -d \$AFP -D .
Minh D (Apr 23 2024 at 14:25):How about if they are not AFP entries, and come from an external source?
Mathias Fleury (Apr 23 2024 at 14:26):You put a ROOTS file in your external one and add another import
Mathias Fleury (Apr 23 2024 at 14:27):like https://github.com/IsaFoL/IsaFoL/blob/master/ROOTS or the one in the AFP
Mathias Fleury (Apr 23 2024 at 14:28):isabelle build -d '$AFP' -d '$ISABELLE_LLVM' -d 'Weidenbach_Book' -D <session_name>
is they way I build my stuff
Minh D (Apr 24 2024 at 05:51):Thank you! I finally got it to build with your suggestions
Last updated: May 06 2024 at 20:16 UTC