Gergely Buday (Jan 04 2021 at 08:26): Gergely Buday (Jan 04 2021 at 08:26):I tried to build a session document for the HOL-IMP session in the HOL library:
src/HOL $ isabelle build -B HOL-IMP
I had to give the [ ... , document = pdf] option. Still, I do not find the generated pdf. There is no output directory.
What shall I do better?
Mark Wassell (Jan 04 2021 at 08:37):Try the build with the -v option.
Gergely Buday (Jan 04 2021 at 08:38):$ isabelle build -v -B HOL-IMP
Started at Mon Jan 4 09:37:36 GMT+1 2021 (polyml-5.8.1_x86_64_32-windows on HP7100-BGergely)
ISABELLE_BUILD_OPTIONS=""
ML_PLATFORM="x86_64_32-windows"
ML_HOME="/cygdrive/d/isabelle/Isabelle2020/contrib/polyml-5.8.1-20200228/x86_64_32-windows"
ML_SYSTEM="polyml-5.8.1"
ML_OPTIONS="--minheap 500"
Session Pure/Pure
Session Tools/Tools
Session HOL/HOL (main)
Session HOL/HOL-Library (main timing)
Session HOL/HOL-IMP (timing)
Session HOL/HOLCF (main timing)
Session HOL/HOLCF-IMP
Finished at Mon Jan 4 09:38:05 GMT+1 2021
0:00:28 elapsed time
What does this tell to you?
Mathias Fleury (Jan 04 2021 at 08:40):I managed to get it to work once, put that command in a Makefile, and never touched the options again: isabelle build -c -o browser_info -B HOL-IMP (you need the '-c' to force recompilation)
Mathias Fleury (Jan 04 2021 at 08:40):That also generates the HTML, but i prefer browsing the HTML file to the pdf file
Gergely Buday (Jan 04 2021 at 10:16):Thanks, @Mathias Fleury I was able to generate the pdf with -c.
Last updated: Dec 21 2024 at 16:20 UTC