Stream: Beginner Questions

Topic: Building a session document


view this post on Zulip 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?

view this post on Zulip Mark Wassell (Jan 04 2021 at 08:37):

Try the build with the -v option.

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Mathias Fleury (Jan 04 2021 at 08:40):

That also generates the HTML, but i prefer browsing the HTML file to the pdf file

view this post on Zulip Gergely Buday (Jan 04 2021 at 10:16):

Thanks, @Mathias Fleury I was able to generate the pdf with -c.


Last updated: Mar 28 2024 at 08:18 UTC