Add interactive library explorer

[VojtechStep]

@JobPetrovcic created an interactive graph for exploring definitions in the library. This PR embeds the explorer on our website.

Some more work is still required outside of this repository, which is why this PR is a draft.

Co-authored-by: Job Petrovčič [email protected]

[VojtechStep]

Status update: we're coordinating with Job, his implementation should now be feature-complete and we're just figuring out some UX details. One of the killer features is tracking deep dependencies; for example, we can now directly see that the proof of funext from univalence doesn't cheat by using funext! The eq-htpy axiom is "observed"/"focused", and the popup says that funext-univalence doesn't contain it in its dependency closure. But it does depend on univalence, as shown in the second screenshot.

[fredrik-bakke]

The WIP interactive explorer can be accessed here: https://jobpetrovcic.github.io/visualize

EDIT: See up-to-date link below.

[fredrik-bakke]

@VojtechStep Can this interactive explorer tell you if a certain rewrite rule was used in the definition of an entry?

[JobPetrovcic]

Oops, I forgot to delete the link you mentioned, @fredrik-bakke. That one is from when we were testing stuff.

Here is the up-to-date link: https://jobpetrovcic.github.io/Unimath-Visualization-Deployment/visualize.html

[fredrik-bakke]

Oh, thank you!

[VojtechStep]

This one is now ready for review. @JobPetrovcic would you check if you're okay with the prose I added around the embedded graph explorer?

Can this interactive explorer tell you if a certain rewrite rule was used in the definition of an entry?

Unfortunately it can't. I'm not in a position to say if Agda stores this information anywhere for it to be possible.

[fredrik-bakke]

I'll try to see if I can find the time tonight to review this PR! 💪

[VojtechStep]

I'll rebase it once I get off work

[fredrik-bakke]

This may be outside the scope of this review so just let me know if that's the case, but would it be possible to make the font usage of the explorer consistent with the library? Consider the six numbered fonts in this image:

Ideally, the fonts at 3, 4, and 6 would be the same as 1, while font 2 and 5 would be the same as our agda code.

(I'm working on a suggested revision of the visualization file, which is why the content is slightly different here)

[EgbertRijke]

This looks great and I very much approve this PR. Very nicely done!

Fredrik made some good suggestions that I second, and I have no further suggestions for changes.

Thank you @JobPetrovcic for this very nice addition to the library!

[VojtechStep]

This may be outside the scope of this review so just let me know if that's the case

Regarding this and other feature requests: Job says he realistically won't be able to work on the underlying explorer until at least February, so that part has a feature-freeze. But he does have the intention to revisit it later, so we should collect feature requests/bugs in the meantime

[fredrik-bakke]

Thanks for the clarification! Where should this be filed?

[JobPetrovcic]

This may be outside the scope of this review so just let me know if that's the case, but would it be possible to make the font usage of the explorer consistent with the library? Consider the six numbered fonts in this image:

Ideally, the fonts at 3, 4, and 6 would be the same as 1, while font 2 and 5 would be the same as our agda code.

(I'm working on a suggested revision of the visualization file, which is why the content is slightly different here)

I can change the fonts. Which fonts do you use? Currently, the visualization uses sans-serif, although 3, I think, does not (unintentionally).

[fredrik-bakke]

@JobPetrovcic The font hierarchy that is specified for agda code in the library is

  --mono-font: Menlo, Source Code Pro, Consolas, Monaco, Lucida Console,
    Liberation Mono, DejaVu Sans Mono, Bitstream Vera Sans Mono, Courier New,
    monospace;

Fonts elsewhere in the HTML seem to be specified via the hierarchy

font-family: "Open Sans", sans-serif

[fredrik-bakke]

Since every further change that was discussed is waiting for changes on the side of Job's, I suggest that we move ahead and merge this. 😁

[JobPetrovcic]

I changed the fonts for 2, 5 to DejaVu Sans Mono and the rest to Open sans.

[fredrik-bakke]

Very nice! Thank you for adding that; I see the changes are live already.

[VojtechStep]

@JobPetrovcic

I changed the fonts for 2, 5 to DejaVu Sans Mono and the rest to Open sans

Unfortunately just changing the font-family to Open Sans doesn't do anything, unless the person viewing the website already has the font installed. We ship the font file at https://unimath.github.io/agda-unimath/fonts/open-sans-v17-all-charsets-regular.woff2 and then have a CSS file containing

@font-face {
  font-family: 'Open Sans';
  font-style: normal;
  font-weight: 400;
  src: local('Open Sans Regular'), local('OpenSans-Regular'),
       url('open-sans-v17-all-charsets-regular.woff2') format('woff2');
}

to define the Open Sans font family. It is not inherited by the iframe.

Also the cascade for --mono-font that we have is written in this way because we accommodate for people having different fonts. If you pick just DejaVu Sans Mono, then people without it installed will likely see a different font used for our codeblocks and the monospace in the explorer.

Again, it's not a problem to leave this until you have more time to spend on the project. Let's not lull ourselves into considering this as implemented.

[JobPetrovcic]

Oh, I did not know that, thank you. I reverted it, although it should take some time (~2h) for the deployment to be set back.

[fredrik-bakke]

Merging now after talking with Vojtech. Thank you so much again for this contribution!

[JobPetrovcic]

Nice! Thank you all for the swift and efficient review.