Zulip Chat Archive

Stream: general

Topic: website build

Rob Lewis (Aug 14 2020 at 11:28):

@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 (Aug 14 2020 at 11:29):

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

Gabriel Ebner (Aug 14 2020 at 11:58):

Oops, shit. I'll take a look.

Gabriel Ebner (Aug 14 2020 at 12:47):

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

Rob Lewis (Aug 14 2020 at 13:00):

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 (Aug 14 2020 at 13:14):

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 (Aug 14 2020 at 13:22):

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

Last updated: Aug 03 2023 at 10:10 UTC