Add diagrams to pdf

[williamdemeo]

Description

Addresses issue #621.

Checklist

• Commit sequence broadly makes sense and commits have useful messages
• Any semantic changes to the specifications are documented in CHANGELOG.md
• Code is formatted according to CONTRIBUTING.md
• Self-reviewed the diff

[WhatisRT]

I think it's best to just make tex files and put them in src/latex. That'll fix the build failures and there's no reason for those to be literate Agda anyway.

[williamdemeo]

I think it's best to just make tex files and put them in src/latex. That'll fix the build failures and there's no reason for those to be literate Agda anyway.

Okay, but I'm not sure how plain tex files should be integrated into the pdf?

I initially put the files under src/latex/Diagrams, as tex files, and then pulled them into the pdf via input lines in a src/latex/Diagrams.tex file, which I \input in Ledger/PDF.lagda, but that doesn't work.

Here's the error I get when running nix-build -A ledger.docs:

Checking that all Agda files have been typechecked...
stat: cannot statx '_build/2.7.0/agda/./latex/Diagrams/ApplyBlock.agdai': No such file or directory
        FAIL: _build/2.7.0/agda/./latex/Diagrams/ApplyBlock.agdai is not up-to-date

[WhatisRT]

I initially put the files under src/latex/Diagrams, as tex files, and then pulled them into the pdf via input lines in a src/latex/Diagrams.tex file, which I \input in Ledger/PDF.lagda, but that doesn't work.

Can you give me the error message for that? That's more or less what I'd expect to work.

Here's the error I get when running nix-build -A ledger.docs:

Checking that all Agda files have been typechecked...
stat: cannot statx '_build/2.7.0/agda/./latex/Diagrams/ApplyBlock.agdai': No such file or directory
        FAIL: _build/2.7.0/agda/./latex/Diagrams/ApplyBlock.agdai is not up-to-date

Yeah, that's because those files are agda files which aren't imported from the top level. Maybe I'll improve the error message on that.

[williamdemeo]

I initially put the files under src/latex/Diagrams, as tex files, and then pulled them into the pdf via input lines in a src/latex/Diagrams.tex file, which I \input in Ledger/PDF.lagda, but that doesn't work.

Can you give me the error message for that? That's more or less what I'd expect to work.

Here's the error I get when running nix-build -A ledger.docs:

Checking that all Agda files have been typechecked...
stat: cannot statx '_build/2.7.0/agda/./latex/Diagrams/ApplyBlock.agdai': No such file or directory
        FAIL: _build/2.7.0/agda/./latex/Diagrams/ApplyBlock.agdai is not up-to-date

Yeah, that's because those files are agda files which aren't imported from the top level. Maybe I'll improve the error message on that.

No, that's the error message I get when I make them .tex files and set it up as you suggested (which, incidentally, is how I tried to integrate the diagrams initially, before switching to .lagda files).

[williamdemeo]

I initially put the files under src/latex/Diagrams, as tex files, and then pulled them into the pdf via input lines in a src/latex/Diagrams.tex file, which I \input in Ledger/PDF.lagda, but that doesn't work.

Can you give me the error message for that? That's more or less what I'd expect to work.

That is the error message I get for that.

Here's the error I get when running nix-build -A ledger.docs:

Checking that all Agda files have been typechecked...
stat: cannot statx '_build/2.7.0/agda/./latex/Diagrams/ApplyBlock.agdai': No such file or directory
        FAIL: _build/2.7.0/agda/./latex/Diagrams/ApplyBlock.agdai is not up-to-date

[williamdemeo]

I somehow forgot to rename the files from .lagda to .tex extension. Integrating the diagrams as tex files works fine now. (I'm not sure what about this is different from the very first time I tried using tex files for the diagrams.)

[WhatisRT]

A few thoughts about the diagrams:

• Pretty much all arrows go back & forth, which is pretty noisy. It's also not clear what an arrow means, so I'd suggest defining the meaning of an arrow first (and explaining it) and then see what should and should't have arrows. Note that something like 'following the thread of the execution' is not a viable meaning here, since the spec doesn't have an execution order.
• What exactly do the colors on the STSs indicate? Is it supposed to mean when it was introduced or when it was last changed? I think last updated would be more useful.
• The types all refer to things as they are called in the implementation, e.g. () instead of ⊤. There's also no PulsingRewardUpdate in the spec, that's an implementation detail.
• There are a bunch of references to implementation details, such as the entry point and which module they are in. These don't make sense here.
• The diagram for conformance testing is nice, but I'm not sure it should be in the spec. I think it would make more sense as a separate little document, possibly with some extra information about conformance testing more generally.
• The Shelley era diagram still looks quite useful to me. I wonder if the most sensible thing to do would be to just update that & include the color information. That means losing the types of the STSs (they wouldn't fit) but I'm not sure how useful they actually are. OTOH if we want to include the types the current split seems sensible but it'd be nice to still provide all the information. For that I think there should be a diagram starting from CHAIN that then references the subtrees that are defined in the other diagrams.