Zulip Chat Archive

Stream: general

Topic: doc-gen is failing


view this post on Zulip Gabriel Ebner (Feb 23 2021 at 20:55):

Just a heads-up, doc-gen has been failing the last two hours: https://github.com/leanprover-community/doc-gen/actions/runs/593756474

view this post on Zulip Bryan Gin-ge Chen (Feb 23 2021 at 21:00):

Looks like it's not able to load export.json for some reason:

Traceback (most recent call last):
  File "print_docs.py", line 713, in <module>
    main()
  File "print_docs.py", line 701, in main
    file_map, loc_map, notes, mod_docs, instances, tactic_docs = load_json()
  File "print_docs.py", line 311, in load_json
    decls = json.load(f, strict=False)
  File "/opt/hostedtoolcache/Python/3.8.7/x64/lib/python3.8/json/__init__.py", line 293, in load
    return loads(fp.read(),
  File "/opt/hostedtoolcache/Python/3.8.7/x64/lib/python3.8/json/__init__.py", line 370, in loads
    return cls(**kw).decode(s)
  File "/opt/hostedtoolcache/Python/3.8.7/x64/lib/python3.8/json/decoder.py", line 337, in decode
    obj, end = self.raw_decode(s, idx=_w(s, 0).end())
  File "/opt/hostedtoolcache/Python/3.8.7/x64/lib/python3.8/json/decoder.py", line 355, in raw_decode
    raise JSONDecodeError("Expecting value", s, err.value) from None
json.decoder.JSONDecodeError: Expecting value: line 1 column 1 (char 0)

view this post on Zulip Eric Wieser (Feb 23 2021 at 21:04):

New lean version? The json serialization changed in master.

view this post on Zulip Bryan Gin-ge Chen (Feb 23 2021 at 21:09):

doc-gen should be using the same version as mathlib though...

view this post on Zulip Bryan Gin-ge Chen (Feb 23 2021 at 21:27):

Hmm, I just ran doc-gen locally with the latest version of mathlib and export.json consists of only this:

doc-gen/src/entrypoint.lean:7:0: error: tactic failed
state:
 true

view this post on Zulip Rob Lewis (Feb 23 2021 at 21:30):

That sounds like mk_export_json is failing. https://github.com/leanprover-community/doc-gen/blob/master/src/export_json.lean#L360

view this post on Zulip Bryan Gin-ge Chen (Feb 23 2021 at 21:31):

Here's the diff between the last working and first failing commits: https://github.com/leanprover-community/mathlib/compare/391c90a3d...f84f5b2e23

view this post on Zulip Rob Lewis (Feb 23 2021 at 21:45):

Too late to troubleshoot tonight. I don't see any obvious issues there. Some missing backticks at https://github.com/leanprover-community/mathlib/compare/391c90a3d...f84f5b2e23#diff-2a1dceda3c5e1bdd94d303d1f1e6fe997ac50f4af68142421c676d0f9f6cd54bR126

view this post on Zulip Bryan Gin-ge Chen (Feb 23 2021 at 22:15):

It seems to be something in category_theory.subobject since the docs build when I renamed the file.

view this post on Zulip Yakov Pechersky (Feb 23 2021 at 22:33):

Could it be due to

section «exists»

or other quoting like that? The section « is the only one I've grepped in mathlib.

view this post on Zulip Bryan Gin-ge Chen (Feb 23 2021 at 22:34):

Doesn't seem to be; I'm gradually commenting out parts of the file and I think I've narrowed it down to something in the module doc.

view this post on Zulip Bryan Gin-ge Chen (Feb 23 2021 at 22:38):

Oh wait, actually I think it's category_theory.mono_over. The very first declaration, of course.

view this post on Zulip Bryan Gin-ge Chen (Feb 23 2021 at 23:00):

OK, I've found the line at which things are breaking, but I don't think I can make any further progress. This line in get_instances is failing on category_theory.mono_over.has_coe which is generated by derive here:

      (expr.const class_nm _)  return e.get_app_fn,

view this post on Zulip Eric Wieser (Feb 23 2021 at 23:06):

I guess the pattern match fails?

view this post on Zulip Eric Wieser (Feb 23 2021 at 23:07):

docs#category_theory.mono_over.has_coe

view this post on Zulip Eric Wieser (Feb 23 2021 at 23:07):

Oh, duh

view this post on Zulip Kevin Buzzard (Feb 23 2021 at 23:13):

So the code which generates the docs is written in Lean??

view this post on Zulip Eric Wieser (Feb 23 2021 at 23:13):

What does #print category_theory.mono_over.has_coe give?

view this post on Zulip Kevin Buzzard (Feb 23 2021 at 23:14):

I had just assumed it was some dumb shell script looking for /-! etc

view this post on Zulip Eric Wieser (Feb 23 2021 at 23:14):

The bit that dumps the metadata is written in lean

view this post on Zulip Kevin Buzzard (Feb 23 2021 at 23:14):

I see!

view this post on Zulip Eric Wieser (Feb 23 2021 at 23:14):

The bit that renders it is python

view this post on Zulip Bryan Gin-ge Chen (Feb 23 2021 at 23:14):

Eric Wieser said:

What does #print category_theory.mono_over.has_coe give?

@[instance]
protected def category_theory.mono_over.has_coe :
  Π {C : Type u₁} [_inst_1 : category C] (X : C),
  (λ (t : Type (max u₁ v₁)), has_coe t (over X)) (mono_over X) :=
λ (C : Type u₁) (_inst_1 : category C) (X : C), coe_subtype

view this post on Zulip Kevin Buzzard (Feb 23 2021 at 23:15):

Maybe you should prove that the lean part works

view this post on Zulip Bryan Gin-ge Chen (Feb 23 2021 at 23:15):

We're all waiting on mm0 for that :joy:

view this post on Zulip Eric Wieser (Feb 23 2021 at 23:18):

Looks like the delta_instances derive_handler doesn't know how to delta-reduce its type

view this post on Zulip Eric Wieser (Feb 23 2021 at 23:18):

Or possibly more insidiously, something about the category theory library makes it not reducible

view this post on Zulip Gabriel Ebner (Feb 24 2021 at 08:35):

Eric Wieser said:

Looks like the delta_instances derive_handler doesn't know how to delta-reduce its type

I think you mean β-reduce. I'm surprised we didn't run into this earlier, derive is used pretty often.

view this post on Zulip Rob Lewis (Feb 24 2021 at 08:49):

I tried to fix it here but there was a deterministic timeout in topology/metric_space/cau_seq_filter that I couldn't reproduce locally. https://github.com/leanprover-community/mathlib/tree/delta-instance-beta

view this post on Zulip Rob Lewis (Feb 24 2021 at 08:49):

Re-running CI in case that was a fluke, not sure what's going on.

view this post on Zulip Rob Lewis (Feb 24 2021 at 08:51):

I think you mean β-reduce. I'm surprised we didn't run into this earlier, derive is used pretty often.

I'm not sure how often we use non-beta-reduced instances with derive, although I would have guessed more than never.

view this post on Zulip Gabriel Ebner (Feb 24 2021 at 08:51):

I'm currently trying to fix the doc-gen side.

view this post on Zulip Eric Wieser (Feb 24 2021 at 08:54):

Rob Lewis said:

I'm not sure how often we use non-beta-reduced instances with derive, although I would have guessed more than never.

We definitely have tests for the non-beta-reduced instances, but I suspect there are no other uses. When I made the change to improve instance names, I was primarily concerned about semimodule R not λ R, semimodule R M, and I only remember fixing references to cases of the former being renamed.

view this post on Zulip Gabriel Ebner (Feb 24 2021 at 08:58):

The doc-gen side is hopefully fixed now.

view this post on Zulip Eric Wieser (Feb 24 2021 at 09:01):

Can we add doc-gen to the #rss stream?

view this post on Zulip Rob Lewis (Feb 24 2021 at 09:02):

@Sebastian Ullrich I think you're in charge of the rss bot, right?

view this post on Zulip Rob Lewis (Feb 24 2021 at 09:02):

https://github.com/leanprover-community/doc-gen

view this post on Zulip Sebastian Ullrich (Feb 24 2021 at 09:03):

Now where did I put the bot...

view this post on Zulip Johan Commelin (Feb 24 2021 at 09:04):

It's under your bed (-;

view this post on Zulip Sebastian Ullrich (Feb 24 2021 at 09:06):

would explain the weird dreams

view this post on Zulip Sebastian Ullrich (Feb 24 2021 at 09:06):

Ok, should work now

view this post on Zulip Rob Lewis (Feb 24 2021 at 09:16):

Rob Lewis said:

I tried to fix it here but there was a deterministic timeout in topology/metric_space/cau_seq_filter that I couldn't reproduce locally. https://github.com/leanprover-community/mathlib/tree/delta-instance-beta

This passed CI this time without changing anything, which is slightly worrying. We don't usually see deterministic timeouts as glitches, do we?

view this post on Zulip Gabriel Ebner (Feb 24 2021 at 09:18):

It's uncommon, but not impossible.

view this post on Zulip Gabriel Ebner (Feb 24 2021 at 09:18):

My gut feeling is that dsimplify is a bit overkill here.

view this post on Zulip Eric Wieser (Feb 24 2021 at 09:21):

I've seen PRs fail with deterministic timeouts then pass after adding an empty commit

view this post on Zulip Rob Lewis (Feb 24 2021 at 09:21):

Gabriel Ebner said:

My gut feeling is that dsimplify is a bit overkill here.

What's better? whnf doesn't do the trick

view this post on Zulip Gabriel Ebner (Feb 24 2021 at 09:36):

I'd use an open_pis + whnf transparency.none + pis

view this post on Zulip Gabriel Ebner (Feb 24 2021 at 14:15):

Hmm, I've just run into the timeout in another PR which does not include your fix: https://github.com/leanprover-community/mathlib/runs/1970111768?check_suite_focus=true

Error: /home/runner/work/mathlib/mathlib/src/topology/metric_space/cau_seq_filter.lean:84:0:
(deterministic) timeout

view this post on Zulip Bryan Gin-ge Chen (Mar 03 2021 at 22:03):

I just pushed a commit to doc-gen and got a notification that the build failed. However, the failure is at the parsing of export.json again and my change to a regex in the markdown rendering shouldn't have affected this at all.

Investigating now...


Last updated: May 12 2021 at 23:13 UTC