Anthony Bordg (Sep 22 2019 at 20:21): Anthony Bordg (Sep 22 2019 at 20:21):Is this the standard way to embed Isabelle code in a LaTeX document ?
Mathias Fleury (Sep 23 2019 at 06:15):If you were to ask Makarius, he would say no. The standard way is to write everything in Isabelle and use the export mechanism to generate the PDF (similar to how all the documentation is generated).
Now, for snippets, I would look at https://isabelle.in.tum.de/dist/Isabelle2019/doc/sugar.pdf, which is more maintained than the community wiki. But I don't think there is any difference in this case.
Anthony Bordg (Sep 23 2019 at 15:17):If you were to ask Makarius, he would say no. The standard way is to write everything in Isabelle and use the export mechanism to generate the PDF (similar to how all the documentation is generated).
Now, for snippets, I would look at https://isabelle.in.tum.de/dist/Isabelle2019/doc/sugar.pdf, which is more maintained than the community wiki. But I don't think there is any difference in this case.
Thanks for the pointer.
The right phrase I wanted to use is not "standard" but "most convenient".
Mathias Fleury (Sep 24 2019 at 06:26):Most convenient: it depends what you want to achieve. For Isabelle documentation, it makes sense to make sure that the snippets are still up-to-date and checked by Isabelle. Therefore, writing LaTeX in Isabelle makes sense (use your development as a base session to make compilation faster).
Now if you do not want to update the Isabelle formalisation for future Isabelle versions or want maximal control over the LaTeX source or want to lie in your paper, then snippets are nicer.
Anthony Bordg (Sep 26 2019 at 17:02):Most convenient: it depends what you want to achieve. For Isabelle documentation, it makes sense to make sure that the snippets are still up-to-date and checked by Isabelle. Therefore, writing LaTeX in Isabelle makes sense (use your development as a base session to make compilation faster).
Now if you do not want to update the Isabelle formalisation for future Isabelle versions or want maximal control over the LaTeX source or want to lie in your paper, then snippets are nicer.
@Mathias Fleury I don't even find in Isabelle the percent sign used in the \text_raw command in section 7.1.
Mathias Fleury (Sep 29 2019 at 06:43):I forgot to open Zulip for a few days…
@Anthony Bordg
It is a normal % sign. See the source file at https://isabelle.in.tum.de/repos/isabelle/file/d4a23cc9aabc/src/Doc/Sugar/Sugar.thy#l521
Anthony Bordg (Sep 29 2019 at 11:24):I forgot to open Zulip for a few days…
Anthony Bordg
It is a normal % sign. See the source file at https://isabelle.in.tum.de/repos/isabelle/file/d4a23cc9aabc/src/Doc/Sugar/Sugar.thy#l521
Thanks Mathias.
Actually, @Angeliki Koutsoukou Argyraki pointed out that the most convenient method, if not the most conventional, consists in taking screenshots of Isabelle (very easy on Mac, press Shift-Command-4) and then use the graphics LaTeX package and in particular its \includegraphics command. So far, I haven't seen any drawback with her method.
Mathias Fleury (Sep 29 2019 at 16:43):It has a few drawbacks:
* you see the real source, which is not always what you want to show in a paper (e.g, «x \in xs» instead of «x \in set xs»)
* you cannot copy-paste the source (which is bad for documentation)
* it is less integrated to the text flow and takes more space.
I have written my Master's thesis in Isabelle but I would not do it again. Since that, I retype everything I want to show in LaTeX directly.
Anthony Bordg (Sep 30 2019 at 11:37):It has a few drawbacks:
* you see the real source, which is not always what you want to show in a paper (e.g, «x \in xs» instead of «x \in set xs»)
You can modify the source before taking the screenshot.
* you cannot copy-paste the source (which is bad for documentation)
I don't clearly see why someone would like to copy-paste your code, anyway it's not a problem if your code is freely available somewhere and you give the link in your article. And as you noted above, what you want to show is not always exactly the real source.
* it is less integrated to the text flow and takes more space.
The graphics package gives a great deal of control on the size of your pictures. Moreover, with the allowed addition of captions I personally think that the text flow is improved.
Mathias Fleury (Sep 30 2019 at 13:06):It has a few drawbacks:
* you see the real source, which is not always what you want to show in a paper (e.g, «x \in xs» instead of «x \in set xs»)
You can modify the source before taking the screenshot.
Only if it is still type correct.
* it is less integrated to the text flow and takes more space.
The graphics package gives a great deal of control on the size of your pictures. Moreover, with the allowed addition of captions I personally think that the text flow is improved.
It depends on the style of writing. If it makes sense, I like when the «raw» version is included within the text flow. (Except when it is HOL. I have yet to be convinced that «MEM x xs» is readable.)
Kevin Kappelmann (Sep 30 2019 at 14:09):another obvious drawback using screenshots: if one changes some part of the formalisation, one might also need to redo the screenshots
Anthony Bordg (Oct 01 2019 at 14:38):another obvious drawback using screenshots: if one changes some part of the formalisation, one might also need to redo the screenshots
It's a good point. Indeed, during the writing of an article you may be led to think harder and improve your formalization.
However there is an easy workaround. Just comment for your memory the code in your LaTeX file where you want to place the screenshots:
%\begin{figure}[H]
% \centering
% \includegraphics[scale=0.5]{}
%\end{figure}
and add your screenshots at the last moment only when your article is completely done and your code stable.
But thanks for your arguments, now I think anyone can make an informed choice.
Lukas Stevens (Oct 02 2019 at 12:26):Screenshots also don't scale nicely, take up a lot of memory, and including them in Latex increases compilation time. I would suggest code listings instead.
Fabian Immler (Oct 19 2019 at 01:07):If you like screenshots, but are worried about scaling them or copy-pasting the underlying source, you can do the following (probably only for the camera ready version):
In Isabelle/jEdit: Plugins->Isabelle->Show Preview in Browser,
then "print" the page in the Browser to get a pdf from which you can cut or crop out your desired "screenshots" as pdf.
Last updated: Apr 19 2024 at 12:27 UTC