Possible bug in Book.py ?

[marcbezem]

When I run Book.py with fresh HoTT/book and HoTT/HoTT, something weird occurs: in the definition of Book_2_2 it substitutes occurrences of "2_1" by "2_2", compromizing the file HoTTBookExercises.v. This file was fine before I ran Book.py. There are a couple of other errors that I don't understand, but probably this part of the diff is sufficient to diagnose the problem (it is of course possible that I did something wrong):

HoTT> diff contrib/HoTTBookExercises.v contrib/HoTTBookExercises.v.bak.1
274,276c274,276
<     (Book_2_2_concatenation1_eq_Book_2_2_concatenation2 p q) *1
<     (Book_2_2_concatenation2_eq_Book_2_2_concatenation3 p q) =
<     (Book_2_2_concatenation1_eq_Book_2_2_concatenation3 p q).
---
>     (Book_2_1_concatenation1_eq_Book_2_1_concatenation2 p q) *1
>     (Book_2_1_concatenation2_eq_Book_2_1_concatenation3 p q) =
>     (Book_2_1_concatenation1_eq_Book_2_1_concatenation3 p q).

Book.py is happy with the labels, but does something that Coq is not happy about.

[mikeshulman]

Exactly what command line are you running, so I can test it?

And what branch/version of HoTT/HoTT are you using? In my copy of upstream/master all these lines already start with Book_2_1.

[marcbezem]

Tomorrow I'll run git show-branch on the desktop I worked on today. Yesterday, I deleted my very old fork (too far behind) and forked afresh, from both HoTT/HoTT and HoTT/book. Part of my work flow is:

cat ../book/*.aux | etc/Book.py contrib/HoTTBook.v
cat ../book/*.aux | etc/Book.py --exercises contrib/HoTTBookExercises.v

The first went fine, the second does the weird thing in Book_2_2 (plus in some others). That definition uses definitions from Section Book_2_1_Proofs_Are_Equal, which are OK, and should read 2_1.

[mikeshulman]

Oh, I misread your diff: I didn't realize that you diffed from the new version to the old version (which is backwards to me), so I thought the change had gone in the opposite direction. Now I see the problem, it's this line in Book.py:

content = re.sub('Book_[0-9_]*[0-9]', 'Book_{0}'.format(book), content)

which is, I guess, trying to "help" the user in case they made the mistake of giving things the wrong name. Presumably whoever wrote this didn't consider the possibility that one definition in one of these files might refer to another one; I think the script was originally written for HoTTBook.v which is intended to consist only of pointers into the library rather than new proofs, whereas in HoTTBookExercises.v which actually contains new proofs it is more reasonable for there to be inter-exercise references.

I would suggest just removing this line from Book.py, as I don't think it is really necessary and I can't think of any easy way to fix it. Any objections?

[marcbezem]

You are right. According to Note 5 in HoTTBook.v, it is a feature, not a bug: "The script renames the Book_X_Y_Z to whatever the correct number is, so initially you can use whatever number you like." :-)

We could do the substitution only when Book_X_Y_Z is preceded by Definition, Proposition, ... Something like:

content = re.sub('Definition Book_[0-9_]*[0-9]', 'Definition Book_{0}'.format(book), content)

(This is not very robust, an extra space between Definition and Book would spoil the thing.)

[mikeshulman]

I suppose.

[andrejbauer]

It was probably me. I think the problem was that the book was still gaining new numbers. Rather than deleting this, I would suggest that people don't run the script on files it was not intended to run on. A good solution would be a command-line argument that turns this feature on or off.

[mikeshulman]

Thanks for the explanation @andrejbauer . We've already merged #924, but we can certainly reopen the question. I'm wary of just having a command-line argument, though, since I expect people will forget, or not know, to add that argument when running on HoTTBookExercises, and get this same very confusing error. Given that the book is no longer gaining new numbers, what would be the reason for keeping this line?

[marcbezem]

The script has been very useful, and there are two files it is intended to run on. It is rather the state of the book that is relevant here. A major change of the numbering (unlikely) would require a run on both files. Adding a label (not an exercise) requires a run of the script on HoTTBook.v. Adding an exercise requires a run on HoTTBookExercises.v. Both can break these files, but the second one is much more likely to do that than the first. True, it was not necessary to run the script on HoTTBookExercises.v after only adding labels. But this detected a problem that would have surfaced anyway after adding an exercise (and this is not an unrealistic event). BTW there is already a switch --exercises. Could that be used to switch off unwanted substitutions?

[mikeshulman]

Wouldn't it be necessary to run the script on HoTTBookExercises after adding a label to an exercise? Or do I misunderstand how the script works?

[marcbezem]

Sure, but I assumed all (new) exercises come with a label for reference, both from the latex version of the solution and from HoTTBookExercises.v. This assumption may have been false.

[mikeshulman]

Many people, including me, are lazy when writing LaTeX and only add labels to environments at the moment when they want to reference them from somewhere else, rather than pre-emptively when the environment is created. If you look through HoTTBook.v you'll see lots of missing numbers, because those theorems/etc. don't have labels yet. I assume the same is true for exercises (such as exercises that don't yet have any solutions provided).