doc-gen is failing

Stream: general

[Gabriel Ebner]

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]

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]

New lean version? The json serialization changed in master.

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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]

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]

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

[Rob Lewis]

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]

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

[Yakov Pechersky]

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]

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]

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

[Bryan Gin-ge Chen]

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]

I guess the pattern match fails?

[Eric Wieser]

docs#category_theory.mono_over.has_coe

[Eric Wieser]

Oh, duh

[Kevin Buzzard]

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

[Eric Wieser]

What does #print category_theory.mono_over.has_coe give?

[Kevin Buzzard]

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

[Eric Wieser]

The bit that dumps the metadata is written in lean

[Kevin Buzzard]

I see!

[Eric Wieser]

The bit that renders it is python

[Bryan Gin-ge Chen]

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]

Maybe you should prove that the lean part works

[Bryan Gin-ge Chen]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Gabriel Ebner]

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]

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]

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

[Rob Lewis]

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]

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

[Eric Wieser]

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]

The doc-gen side is hopefully fixed now.

[Eric Wieser]

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

[Rob Lewis]

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

[Rob Lewis]

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

[Sebastian Ullrich]

Now where did I put the bot...

[Johan Commelin]

It's under your bed (-;

[Sebastian Ullrich]

would explain the weird dreams

[Sebastian Ullrich]

Ok, should work now

[Rob Lewis]

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]

It's uncommon, but not impossible.

[Gabriel Ebner]

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

[Eric Wieser]

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

[Rob Lewis]

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]

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

[Gabriel Ebner]

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]

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...