Stream: Beginner Questions

Topic: Isabelle LaTeX documents

view this post on Zulip waynee95 (Oct 20 2022 at 09:32):

I want to embed LaTeX into the main formalization file to explain and highlight the important proofs and explain design decisions. So unnecessary proofs will be hidden in the rendered pdf.

Now I am wondering how I can have an Appendix with the full formalization without copying the whole file twice and removing the embedded LaTeX and remove the comments to make the other parts non hidden

view this post on Zulip Jonathan Julian Huerta y Munive (Oct 20 2022 at 12:22):

I've seen that you can "tag" certain Isabelle commands and use those tags to generate the .pdf in a customised way. For instance, if you use tags %exercise and %solution as shown below:

text_raw %exercise ‹ \pagebreak[3] ›

lemma %solution "a * b = b * (a :: nat)"
  by simp

lemma "add n 0 = n"
  apply %solution (induction n)
   apply simp_all
  done

and if your ROOT file contains something like:

session "session_name" = Main +
  options [document = pdf,  document_output = "output",
     document_variants="exercise_pdf_name=+exercise,-solution:solution_pdf_name=+solution,-exercise"]
  theories
    theory_name
  document_files (in "../document")
    "root.tex"

Then there will be two generated pdfs. One called exercise_pdf_name showing things tagged with %exercise but not with %solution (notice the + and the -), and one called solution_pdf_name showing those tagged with %solution but not with %exercise.

There is also the %invisible tag that seems to be automatically skipped in the .pdf generation process. My knowledge on this is only practical, so if anyone can complement with the correct description of how tagging works, I would gladly learn more. I hope this is useful.

view this post on Zulip Emin Karayel (Apr 18 2023 at 13:01):

Is there a convention for referencing certain facts/definitions in already submitted AFP entries in another publication:

I usually write something like "lemma left_id~\cite[Sect. 1]{Hello_World-AFP}" which then becomes:
lemma left_id [Sect. 1,xy]

Here: Hello_World-AFP is the bibtex entry from the AFP.

The problem with this solution is that it requires multiple steps for someone to actually find the corresponding lemma, when looking it up. (Open the outline, look for the right section, find the corresponding lemma.)

It would technically be possible to use a hyperref to directly link to it, i.e. something like:
\href{https://www.isa-afp.org/theories/hello_world/#IO.html#IO.left_id|fact}{lemma left_id}

However, I am worried the latter may fail after possible changes on the website, i.e. it doesn't seem to be a permalink.
What is the best approach, here?

view this post on Zulip Lukas Stevens (Apr 18 2023 at 13:15):

What is the result if you use document antiquotations such as @{thm left_id}? This requires you to import the entry, though.

view this post on Zulip Emin Karayel (Apr 18 2023 at 13:31):

Thanks, though in this case I don't have an isabelle theory to cite from. I want to reference an entity from a paper (that is not an Isabelle document).

For example, when you cite a lemma from a paper in a different paper, you would usually write:
\cite[Lemma 2.1]{agrawal2004}

I would like to do the same thing from a paper into a lemma in an AFP Entry.

view this post on Zulip Fabian Huch (Apr 18 2023 at 15:29):

IMHO the best option currently is to cite the entry (the AFP is a dblp-indexed journal after all) and the definition/lemma number in that entry, which you can define and keep consistent yourself (assuming you are the entry author). All other options are not stable.

Last updated: Apr 24 2024 at 12:33 UTC