website build

Stream: general

[Rob Lewis]

@Gabriel Ebner the website build is failing here because of changes to doc-gen. the json file that doc-gen creates now contains a lot of junk that I guess is for the formatting:

['n', ['c', '\ue000irrational\ue001irrational\ue002', ['n', ['c', '\n', ['n', ['n', ['c', ['c', '(', ['n', ['c', '\ue000real.sqrt\ue001real.sqrt\ue002', ['n', '\n2']]]], ')']]]]]]]

Is it possible to erase that before the json export?

[Rob Lewis]

I can take a look later but don't have time right now.

[Gabriel Ebner]

Oops, shit. I'll take a look.

[Gabriel Ebner]

https://github.com/leanprover-community/doc-gen/pull/49 and https://github.com/leanprover-community/leanprover-community.github.io/pull/111

[Rob Lewis]

Nice, thanks. This is removing a bit of semantic info, instead of giving a list of args it's throwing everything into one string. A tool that wants to show only explicit args, for example, will have to do some html parsing. But that's a hypothetical and this is also adding useful information (the links), so I think it's more than worth it.

[Gabriel Ebner]

We could add the string version back, but I'm not sure if the documentation export file is the right place to store all this data. Note that you can easily hide the implicit arguments using css if you want (.impl_arg { display: none; }).

[Rob Lewis]

Yeah, that's fair, I'm fine with the change.