Stream: General

Topic: missing isabelle component

view this post on Zulip zibo yang (Jul 05 2021 at 03:11):

Is there anyone who can help me with this problem?

hp@LAPTOP-K1JS8QU4 ~/Desktop/Isabelle2021
$ isabelle mkroot -A LATEX gambler
### Missing Isabelle component: "/cygdrive/c/Users/hp/.isabelle/Isabelle2021/~/afp/afp-2021-05-14/thys"

Preparing session "gambler" in "gambler"
  creating "gambler/ROOT"
  creating "gambler/document/root.tex"

Now use the following command line to build the session:

  isabelle build -D gambler


hp@LAPTOP-K1JS8QU4 ~/Desktop/Isabelle2021
$ isabelle components -a
### Missing Isabelle component: "/cygdrive/c/Users/hp/.isabelle/Isabelle2021/~/afp/afp-2021-05-14/thys"
Skipping existing component "/cygdrive/c/Users/hp/Desktop/Isabelle2021/afp/afp-2021-05-14/thys"

how to get this component back?

view this post on Zulip Mathias Fleury (Jul 05 2021 at 05:43):

in your settings or components file, the path to AFP is wrong

view this post on Zulip Mathias Fleury (Jul 05 2021 at 06:43):

/cygdrive/c/Users/hp/.isabelle/Isabelle2021/~/afp/afp-2021-05-14/thys
should be something else. And use an absolute path without ~.

view this post on Zulip zibo yang (Jul 05 2021 at 12:42):

Mathias Fleury said:

/cygdrive/c/Users/hp/.isabelle/Isabelle2021/~/afp/afp-2021-05-14/thys
should be something else. And use an absolute path without ~.

Well, but when I change my path to absolute one like:

#bundled components
contrib/bash_process-1.2.3-1
contrib/bib2xhtml-20190409
contrib/csdp-6.1.1
contrib/cvc4-1.8
contrib/e-2.5-1
contrib/flatlaf-1.0
contrib/isabelle_fonts-20190717
contrib/jdk-15.0.2+7
contrib/jfreechart-1.5.1
contrib/jortho-1.0-2
contrib/kodkodi-1.5.6
contrib/nunchaku-0.5
contrib/opam-2.0.7
contrib/polyml-test-f86ae3dc1686
contrib/postgresql-42.2.18
contrib/scala-2.13.4-1
contrib/smbc-0.4.1
contrib/spass-3.8ds-2
contrib/sqlite-jdbc-3.34.0
contrib/ssh-java-20190323
contrib/stack-2.5.1
contrib/vampire-4.2.2
contrib/verit-2020.10-rmx-1
contrib/xz-java-1.8
contrib/z3-4.4.0pre-3
contrib/zipperposition-2.0-1
contrib/sumatra_pdf-3.1.2-2
contrib/naproche-755224402e36
C:/Users/hp/Desktop/Isabelle2021/afp/afp-2021-05-14

then isabelle stop resolving any theory in AFP.
Previous it 's "afp/afp-2021-05-14/thys" as relative one but it works well.

view this post on Zulip zibo yang (Jul 05 2021 at 13:00):

Fine, I code the right absolute path here.

view this post on Zulip zibo yang (Jul 05 2021 at 13:08):

hp@LAPTOP-K1JS8QU4 ~/Desktop/Isabelle2021/gambler
$ isabelle mkroot
### Missing Isabelle component: "/cygdrive/c/Users/hp/.isabelle/Isabelle2021/~/afp/afp-2021-05-14/thys"

Preparing session "gambler" in "."
  creating "ROOT"
  creating "document/root.tex"

Now use the following command line to build the session:

  isabelle build -D .


hp@LAPTOP-K1JS8QU4 ~/Desktop/Isabelle2021/gambler
$ isabelle components -a
### Missing Isabelle component: "/cygdrive/c/Users/hp/.isabelle/Isabelle2021/~/afp/afp-2021-05-14/thys"
Skipping existing component "/cygdrive/c/Users/hp/Desktop/Isabelle2021/afp/afp-2021-05-14/thys"

I change my path as

/cygdrive/c/Users/hp/Desktop/Isabelle2021/afp/afp-2021-05-14/thys

but it still fails like above, so what's wrong with that?

view this post on Zulip zibo yang (Jul 05 2021 at 13:29):

Ok now I guess I solve this missing component problem:

hp@LAPTOP-K1JS8QU4 ~/Desktop/Isabelle2021/gambler
$ isabelle mkroot

Preparing session "gambler" in "."
  creating "ROOT"
  creating "document/root.tex"

Now use the following command line to build the session:

  isabelle build -D .
hp@LAPTOP-K1JS8QU4 ~/Desktop/Isabelle2021/gambler
$ isabelle build -o document=pdf -P output -D .
Presentation in "/cygdrive/c/Users/hp/Desktop/Isabelle2021/gambler/output"
Presenting gambler ...
0:00:05 elapsed time

However, my document.pdf is nothing but title and my ROOT shows like:

session gambler = HOL +
  options [document = pdf, document_output = "output"]
(*theories [document = false]
    A
    B
  theories
    C
    D*)
  document_files
    "root.tex"

Now I want to figure out why it produces an empty pdf?

view this post on Zulip Wenda Li (Jul 05 2021 at 13:57):

Your ROOT file does not seem good, it should have at least one theory file you intend to build.

view this post on Zulip zibo yang (Jul 05 2021 at 14:13):

Yes I agree, but why does it produce such "empty" ROOT?

view this post on Zulip Wenda Li (Jul 05 2021 at 14:22):

mkroot simply creates an empty entry. What you need to do is to put your development in this entry, say it is D.thy, then you modify the ROOT file:

  options [document = pdf, document_output = "output"]
  theories
    D
  document_files
    "root.tex"

Finally, you can try to build the entry as you were attempting, which should results in a pdf for D.thy.

Last updated: Apr 23 2024 at 08:19 UTC