# IRC log for #isabelle, 2017-04-30

All times shown according to UTC.

Time Nick Message
01:04 ertes joined #isabelle
07:30 JCaesar There's also different opinions among mathematicians on what should be called a corollary and what shouldn't.
11:21 ammbauer are the HTML docs also available online for the development version of isabelle? like here https://isabelle.in.tum.de/dist/library/HOL/index.html
11:22 larsrh I don't think so
11:22 larsrh Jenkins doesn't generate them
11:23 larsrh no wait, actually it does ^^
11:23 larsrh https://ci.isabelle.systems/jenkins/job/isabelle-repo-makeall/ws/browser_info/index.html
11:27 ammbauer https://ci.isabelle.systems/jenkins/job/isabelle-repo-makeall/ws/browser_info/HOL/HOL-Decision_Procs/Commutative_Ring_Ex.html
11:27 ammbauer larsrh: well, now you can improve your answer on stack overflow and promote jenkins :D
11:27 ammbauer some of those lemmas are really… … cringy :D
11:28 larsrh which one?
11:29 ammbauer http://stackoverflow.com/a/43704252
11:29 larsrh But the «» syntax is not defined there
11:29 larsrh oh, now I get it
11:32 larsrh done
11:35 pruvisto is this guillemet syntax some fancy magic to embed natural numbers into a ring?
11:37 larsrh a ring to embed them, in the darkness to divide them
11:37 larsrh I'll show myself out
11:39 pruvisto >_>
12:43 mbrcknl joined #isabelle
15:18 ertes joined #isabelle
18:06 ertes joined #isabelle
18:24 ezyang joined #isabelle
19:12 mal joined #isabelle
20:18 chindy Assume I have a theory in my current directory, called MyProof.thy . how do I have to write my ROOT file such that i can generate latex snippets etc ?
20:24 chindy with this root file where also tried with "HOL" instead of "HOL-Analysis" the proof fails when running build -D .   http://downthetypehole.de/paste/p4ayHe58
20:27 int-e isabelle mkroot -d  prepares a ROOT file and a document subdirectory, which may be an easier starting point than just a ROOT file.
20:28 int-e (in fact I don't know the layout of the document subdirectory by heart because this command exists)
20:28 chindy int-e: yea i did that before
20:29 chindy problem is the running
20:29 chindy problem is the running build tells me that it failed to build document
20:29 int-e okay, well "fails" is not a useful symptom to diagnose.
20:29 chindy int-e: true...
20:30 int-e look at the log file (it's in the error message); there should be a latex error near the end. you may have to edit the root file and enable one or more of the commented \usepackage commands.
20:31 int-e but it's also possible that your .thy file contains some latex syntax error.
20:31 chindy do i need to do anything in my thy file. Because the only thing i have are section \open \close and text \open \close
20:33 chindy okay apparently ./output/document/root.pdf seems to contain something, but ./output/document.pdf is literally just one page with the name of the theory as title.
20:37 chindy Is it possible to acquire latex code for specific proofs/definitions etc... to include in a thesis?
20:37 int-e there are recipes for creating "snippets" around, hmm.
20:39 int-e https://isabelle.in.tum.de/community/Generate_TeX_Snippets
20:41 pruvisto honestly I never use that at all
20:41 pruvisto I don't like the way these generated LaTeX loops
20:41 pruvisto *looks
20:41 int-e loops?
20:41 int-e oh, looks
20:41 pruvisto besides, I usually change the notation to make it more accessible to non-Isabelle users
20:42 pruvisto so I just typeset the LaTeX myself from scratch
20:43 chindy pruvisto: so you just incldue the latex code in a paper using minted or lstlisting... ?
20:48 pruvisto I don't think you can use maths mode in that
20:48 pruvisto no, I usually use something like the "align*" environment
20:49 pruvisto \begin{align*} &\textbf{lemma}\ \text{length}\ (x\#\textit{xs}) = \text{Suc}\ (\text{length}\ \textit{xs})
20:49 pruvisto etc.
20:49 pruvisto something like that
20:49 pruvisto no idea if that is the best way to do this stuff
20:50 pruvisto but I usually try not to have /too/ much Isabelle code on slides and in papers, so it's not that important
20:52 int-e Well, personally I like the idea that using snippets prevents typos. But that said, I haven't used them much and the last time I ended up adjusting whitespace in the generated output... and there was quite a bit of custom latex notation. So it's a mixed blessing.
20:56 pruvisto true
20:57 pruvisto I just noticed that I was so dissatisfied with the LaTeX output that I would have to adjust too much
20:57 pruvisto In my opinion, we're still a long way from the ideal that you "write" your papers in Isabelle
20:58 ertesx joined #isabelle
23:16 chindy what method does smt use, that it appears to(very often at least) reconstruct a proof of this type: show ?thesis by linarith (* failed *)