Automatically generate sections describing Unicode input

[ywata]

Regarding #211, I created simple script to generate unicode instructions. I reorganize the structure of code so that it is useable to update PLFA.

The script is one parameter how to generate instructions. It changes how many times we show instructions in chapter to chapter. Ex. \bN is used Naturals.lagda, Induction.lagda, Relation.lagda and etc.

We do not have to show the instruction in every chapter and I think 2 or 3 times is reasonable. I created two branches to compare them, let me know your opinion:

• unicode-2times
• unicode-3times

My personal preference is 3 for Part 1 and 1 or 2 for Part 2, because we have many things to memorize in Part 1 and the instructions helped me a lot, on the other hand when we continue to read Part 2, I think it's better for readers to check agda-input.el by themselves. Let me know your opinion for the parameter. I'll send a pull request for the script based on your opinion.

(Note: My script only checks unicode characters that appeared in a file, I do not care whether the character is used in the exercises or not.)

I would also like to know where I put files. Now I have 3 files:

1. perl script to generate unicode instructions using following files;
2. text file that contains all the lagda file to be examined in chapter order;
3. text file that contains unicode instructions for each character.

My guesses are that 1 will be plfa.github.io/bin and 2 and 3 will be in plfa.github.io/src/plfa.

[wenkokke]

@wadler What do you think about this? I think @ywata makes a great suggestion to repeat the new unicode characters several times in Part 1 of the book, and automating this would be useful when we expand the book, and to guarantee consistency.

[wadler]

@ywata I am impressed! Nice idea. Thank you.

Yes, I like the proposal to repeat characters three times in Part I and twice in Part II.

Am I right that this has the disadvantage that when you are editing the source file you no longer see the Unicode instructions in the source you are editing? This is a minor drawback, but on balance I think we could live with it.

I leave it to @wenkokke to confirm that everything is in order related to all the other software used to generate PLFA.

[wenkokke]

@wadler I don't think this is right, we've not integrated it with the Makefile. However, you raise a good point. Should we integrate it with the makefile, so that the unicode listings are automatically updated when we change the paper? I think the main reason there were bugs in there to begin with is because we've changed the source/text of the chapters without constantly maintaining them, so I'd be in favor of this. The downside is that we'd add perl as a dependency to the build process.

[ywata]

I created a branch based on this issue. https://github.com/ywata/plfa.github.io/tree/pr-06

I also created a repository of unicode instruction generator in https://github.com/ywata/plfa_tool/unicode_instruction