Zulip Chat Archive

Stream: general

Topic: website build


view this post on Zulip 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?

view this post on Zulip Rob Lewis (Aug 14 2020 at 11:29):

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

view this post on Zulip Gabriel Ebner (Aug 14 2020 at 11:58):

Oops, shit. I'll take a look.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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; }).

view this post on Zulip Rob Lewis (Aug 14 2020 at 13:22):

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


Last updated: May 12 2021 at 23:13 UTC