Zulip Chat Archive

Stream: general

Topic: doc-gen is failing


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

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)

Eric Wieser (Feb 23 2021 at 21:04):

New lean version? The json serialization changed in master.

Bryan Gin-ge Chen (Feb 23 2021 at 21:09):

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

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

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

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

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

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.

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.

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.

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.

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,

Eric Wieser (Feb 23 2021 at 23:06):

I guess the pattern match fails?

Eric Wieser (Feb 23 2021 at 23:07):

docs#category_theory.mono_over.has_coe

Eric Wieser (Feb 23 2021 at 23:07):

Oh, duh

Kevin Buzzard (Feb 23 2021 at 23:13):

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

Eric Wieser (Feb 23 2021 at 23:13):

What does #print category_theory.mono_over.has_coe give?

Kevin Buzzard (Feb 23 2021 at 23:14):

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

Eric Wieser (Feb 23 2021 at 23:14):

The bit that dumps the metadata is written in lean

Kevin Buzzard (Feb 23 2021 at 23:14):

I see!

Eric Wieser (Feb 23 2021 at 23:14):

The bit that renders it is python

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

Kevin Buzzard (Feb 23 2021 at 23:15):

Maybe you should prove that the lean part works

Bryan Gin-ge Chen (Feb 23 2021 at 23:15):

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

Eric Wieser (Feb 23 2021 at 23:18):

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

Eric Wieser (Feb 23 2021 at 23:18):

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

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.

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

Rob Lewis (Feb 24 2021 at 08:49):

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

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.

Gabriel Ebner (Feb 24 2021 at 08:51):

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

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.

Gabriel Ebner (Feb 24 2021 at 08:58):

The doc-gen side is hopefully fixed now.

Eric Wieser (Feb 24 2021 at 09:01):

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

Rob Lewis (Feb 24 2021 at 09:02):

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

Rob Lewis (Feb 24 2021 at 09:02):

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

Sebastian Ullrich (Feb 24 2021 at 09:03):

Now where did I put the bot...

Johan Commelin (Feb 24 2021 at 09:04):

It's under your bed (-;

Sebastian Ullrich (Feb 24 2021 at 09:06):

would explain the weird dreams

Sebastian Ullrich (Feb 24 2021 at 09:06):

Ok, should work now

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?

Gabriel Ebner (Feb 24 2021 at 09:18):

It's uncommon, but not impossible.

Gabriel Ebner (Feb 24 2021 at 09:18):

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

Eric Wieser (Feb 24 2021 at 09:21):

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

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

Gabriel Ebner (Feb 24 2021 at 09:36):

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

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

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: Dec 20 2023 at 11:08 UTC