2020-04-07 14:4:46 (GMT)
What is the isabelle command line to compile document/root.tex to generate a pdf document? When I try isabelle latex -o pdf in the document folder it simply tells me isabelle.sty is missing. Is such a package available somewhere?
2020-04-07 14:11:44 (GMT)
Now I am trying with isabelle document in the main thy folder and I get the error
Latex error: File `session.tex' not found.
2020-04-07 14:15:44 (GMT)
I never remember by heart what needs to be done.
2020-04-07 14:15:51 (GMT)
And the system manual is hard to read.
2020-04-07 14:16:10 (GMT)
But roughly, you can motify ROOT to generate documentation.
2020-04-07 14:17:34 (GMT)
Something like this:
options [document = pdf, document_output = "output",
document_variants = "document:outline=/proof,/ML"]
2020-04-07 14:18:1 (GMT)
At least the first part:
options [document = pdf, document_output = "output"]
2020-04-07 14:18:49 (GMT)
If you look at Unordered_Resolution in IsaFoL, you'll see an example. Try to reproduce it. That's how I normally do it.
2020-04-07 14:20:50 (GMT)
I always look at the Makefile in the IsaFoL repo:
$(RUN_ISABELLE2017) build -d '$AFP' -o browser_info -o "document=pdf" -v -b -D GRAT/gratchk
(it also generates the HTML version)
2020-04-07 14:33:30 (GMT)
Thanks a lot! It seems to work (now I just need to understand why the table of content is empty...)
2020-04-07 14:42:25 (GMT)
Do you have chapter/section/subsection in your development?
2020-04-07 14:43:52 (GMT)
No. Good point. I suppose I should add section headers at the beginning of each file.
2020-04-07 14:52:51 (GMT)
Ideally, also one little paragraph per file. I'd say that's a minimum so that readers find their way around your document.
2020-04-07 14:53:19 (GMT)
(My job title used to be "documentation manager", for three years, so I feel like it's my duty to write such things. Sorry!)
2020-04-07 14:53:50 (GMT)
I'd be happy to check your PDF once it's ready (if you don't mind my complaining about it afterwards) :S
2020-04-07 15:20:19 (GMT)
That would be great. Do you want only the pdf or rather the whole archive?
2020-04-07 15:23:9 (GMT)
You can send the whole archive.
2020-04-07 21:44:21 (GMT)
It can be downloaded here: https://nextcloud.mpi-klsb.mpg.de/index.php/s/JiLSNdLQNoKxSiw
2020-04-07 21:48:48 (GMT)
I will be glad for any feedback, but don't expect any reaction from me tomorrow, I most certainly won't be available for work.
2020-04-08 7:41:42 (GMT)
Abstract:
saturation calculi, such as ordered resolution or superposition, and allows [add missing comma]
2020-04-08 7:42:17 (GMT)
I'd lowercase "Given Clause loop"
available at http://matryoshka.gforge.inria.fr/pubs/satur_report.pdf . [remove spurious space before .].
2020-04-08 7:42:36 (GMT)
TOC:
2020-04-08 7:43:15 (GMT)
1.1 is plural, 1.2 and 1.3 are singular. I'd standardize on plural.
2020-04-08 7:44:3 (GMT)
Consequence Relation Family -> Families of Consequence Relations
[more natural -- but of course the Isabelle identifier is OK as is]
2020-04-08 7:44:33 (GMT)
Calculi with a Redundancy Criterion
2020-04-08 7:44:51 (GMT)
2.2. Calculi with a Family of Redundancy Criteria
2020-04-08 7:45:41 (GMT)
What is "strong standard lifting"?
2020-04-08 7:46:16 (GMT)
I have trouble parsing "Using an Empty Order to Obtain Results with Orderings".
2020-04-08 7:47:35 (GMT)
Does this mean "Specializing Results Involving Orderings with the Empty Ordering" or something like that? And why "order" vs. "ordering"?
2020-04-08 7:48:17 (GMT)
You can use either word, but use it consistently. Uwe went for "ordering" so we're using that consistently in the paper/report. In the papers on HO superposition, we went for "order".
2020-04-08 7:48:38 (GMT)
(To me a "partial order" sounds natural and a "partial ordering" weird. But I can live with both.)
2020-04-08 7:50:18 (GMT)
"Generic Prover Architecture" is not something we have in the paper. I'm sure it's useful, but it deserves more explanation.
2020-04-08 7:54:25 (GMT)
Body:
It would be nice if the notions of inference system of AFP entry "Ordered_Resolution_Prover" could be merged with yours. Your version is better (more general and more uniform), so I wouldn't mind porting to it. Maybe we can discuss such restructuring once the proof is in the AFP? And maybe once some progress on soundness has been made.
2020-04-08 7:55:37 (GMT)
I'd really like things like the counterexample-reducing inference systems (which are used to prove typically ground completeness -- something where Waldmann et al. provides nothing and hence where we have to turn to B&G 2001) to be part of the same formal framework (if not the same AFP entry).
2020-04-08 7:56:36 (GMT)
In section 2, keep in mind that Uwe is soon going to add a section 2.5. I expect it will be easy to formalize.
2020-04-08 7:56:57 (GMT)
You can add it once it's in the AFP. (I can make the actual change to the repository then.)
2020-04-08 7:57:19 (GMT)
Since we want the AFP submission to happen soon -- before the IJCAR deadline.
2020-04-08 7:59:34 (GMT)
infinitely descending loop of sublocales -> infinitely descending chain of sublocales
[divergence != loop]
2020-04-08 8:8:28 (GMT)
the fourth section of -> section 4 of
2020-04-08 8:27:36 (GMT)
Source files:
I wouldn't define empty order. Instead, you can write (%_ _. False). That's
what everybody would do in this situation, which explains why this fundamental
concept is not already defined in HOL (to the best of my knowledge). If you
really prefer the name "Empty_Order" (not sure why the capitals), you can
introduce it as an abbreviation.
You sometimes have two blank lines between theorems, with no visible reason. It
seems to be an artifact of the (* *) comments. I'm starting to think that
perhaps it would be better to use a formal "text ⟨ ⟩" command, maybe with a
prefix like "Report label: thm:foo-bar." It would make the document look a bit
less naked. Once the report has been published as a journal article (in a
couple of yeas), we can replace all of those with actual numbers. (I could
automate this process, I think.) If one of the AFP editors ask questions, tell
them it's temporary and point them to
http://matryoshka.gforge.inria.fr/pubs/saturate_report.pdf
which still has the LaTeX names in the margin.
It's generally good style to avoid lines longer than 80 or 100 characters for
code (and 80 for text). jEdit has an indicator at the bottom that tells you how
far you are. Sticking to the 100-character convention makes it easier for
readers to inspect the sources---they can focus on scrolling in a single
direction---and will lead to fewer (if any) bad line breaks in the generated
PDF document.
Some of your files have spurious trailing whitespace. These often end up
causing trouble in public repositories---e.g. somebody's editor removes them
automatically and the diff becomes big. Best to remove them. See e.g.
https://www.gnu.org/software/emacs/manual/html_node/emacs/Useless-Whitespace.html
2020-04-08 8:28:8 (GMT)
That's it. This is very impressive stuff. I'm particularly excited about the LGC architecture!
2020-04-08 20:16:30 (GMT)
Thanks a lot! :big_smile:
2020-04-08 20:16:39 (GMT)
Jasmin Blanchette said:
What is "strong standard lifting"?
It corresponds to Remark 22 in the report. I'll move it closer to the standard lifting, and add an isalabel there to make the connection clear.
2020-04-08 20:36:37 (GMT)
Jasmin Blanchette said:
"Generic Prover Architecture" is not something we have in the paper. I'm sure it's useful, but it deserves more explanation.
The beginning of section 4.1 (Given Clause Procedure), including lemma 58 and 59, introduces results that hold for both architecture (and any other build on the same principle). In particular, lemma 59 is useful in both GC and LGC so it makes sense to have this part as its own locale. In fact, in the report, it could also make sense to introduce this subsection (but it is relatively small, so I'll let you judge on that).
2020-04-08 21:54:16 (GMT)
I have replaced the definition of (Labeled_)Empty_Order with an abbreviation.
2020-04-09 7:43:11 (GMT)
Jasmin Blanchette said:
In section 2, keep in mind that Uwe is soon going to add a section 2.5. I expect it will be easy to formalize.
I think I missed a discussion there. What are you referring to?
2020-04-09 7:51:13 (GMT)
Uwe wrote a very long email on 7 April at around midnight, titled "Re: Saturation framework, status". That's what I'm referring to.
2020-04-09 8:8:59 (GMT)
Ah, I found it. I guess the last part about the fixed set of formulas, that is calculus independent, will indeed need to be added to the framework.
2020-04-09 8:14:25 (GMT)
But since it is anyway possible to modify an entry after it is in the AFP, I will proceed with the submission now.
2020-04-09 8:19:43 (GMT)
Of course, go ahead.
2020-04-09 8:20:6 (GMT)
BTW this TODO item is fixed, right?
* Remove obsolete text like this in the formalization: (ST)
text \<open>thm:gc-completeness\<close>
text \<open>The completeness statement below is not identical to that of
the paper. The formalization showed that the paper statement was too
strong. The following statement corresponds better to what happens in
practice and the paper will be updated accordingly before the final version
is published\<close>
2020-04-09 8:22:1 (GMT)
Normally yes.
2020-04-09 8:26:45 (GMT)
OK.
2020-04-09 8:27:0 (GMT)
And you're one lemma away from finishing this item, right?
* Finish putting Isabelle lemma names in margin instead of LaTeX ref. (ST)
2020-04-09 8:27:29 (GMT)
(The deadline is next week, so I'm starting to apply some pressure on my coauthors...)
2020-04-09 8:29:51 (GMT)
I thought I had all of them. Which lemma is still missing?
2020-04-09 8:30:19 (GMT)
grep showlabel will tell you
2020-04-09 8:30:43 (GMT)
Ah it's a typo I guess.
2020-04-09 8:30:56 (GMT)
Ok. This is the next item on my todo list then.
2020-04-09 8:31:10 (GMT)
You wrote \showlabel instread of \isalabelmaybe?
2020-04-09 8:31:27 (GMT)
Indeed. I can fix it.
2020-04-09 8:32:55 (GMT)
LaTeX has such a messy syntax: when you pass arguments to a macro taking arguments, it usually doesn't complain and does something really weird.