Tactic regression tests via mathport

Stream: lean4

[Jannis Limperg]

I wrote a first draft of an extension to mathport that translatesTacticInvocations into regression tests. Code here: https://github.com/JLimperg/mathport

However, I haven't managed to actually test this extension yet. When I run the modified mathport, it reports 0 tactic invocations parsed by parseAST3. I think I followed the build instructions, using the latest release with download-release.sh. Any idea what's going wrong?

[Jannis Limperg]

For reproduction: I tried roughly

make build
make source
./download-release.sh nightly-2022-07-18
make TARGET=data.list.basic port-mathbin-single

[Jannis Limperg]

After some more investigation, it seems like the tactic invocations are never exported to the .ast.json files. E.g. data/vector.lean contains some tactic calls, but data/vector.ast.json does not have a tactics section (or at least grep doesn't find tactics there). This also applies when I delete the sources downloaded via download-release.sh and run make predata myself. @Mario Carneiro are the tactic invocations supposed to be there?

[Mario Carneiro]

You have to explicitly enable it, they aren't there by default because the data gathering is expensive

[Mario Carneiro]

looks like you need to do lean --make --ast --tsast if you want tactic states

[Mario Carneiro]

If we're going to be using this data regularly in mathport we should probably enable that flag in the CI that generates the ast.json files

[Jannis Limperg]

Nice, thanks! I'll first test the whole thing locally and then we can talk about CI integration and so on.

[Jannis Limperg]

The --tsast works, but unfortunately I get a segfault during predata generation:

$ make predata
...
cd sources/mathlib && lean --make --recursive --ast --tlean src
/home/jannis/.nocdp/mathport/sources/mathlib/src/logic/basic.lean: exists_eq_right'make: *** [Makefile:79: mathbin-predata] Segmentation fault

This also seems to happen with a fresh checkout of mathport master and without --tsast, though I need to test it from scratch to be sure I didn't mess anything up. In the meantime, any suggestions?

[Mario Carneiro]

Is that a segfault in the lean invocation?

[Mario Carneiro]

can you run it without the makefile?

[Jannis Limperg]

Yes, it's Lean:

$ cd sources/mathlib/
$ find -name "*.olean" -delete
$ lean --make --recursive --ast --tlean src
/tmp/mathport/sources/mathlib/src/logic/basic.lean: forall_eq_apply_imp_ifffish: Job 1, 'lean --make --recursive --ast -…' terminated by signal SIGSEGV (Address boundary error)

This is on a fresh checkout of mathport master.

[Jannis Limperg]

With mathlib3 commit 903e8941f0862f6c34f28babbb607842a7f8a6c7 (the last on July 18th, when the last mathport release was made), there seems to be no segfault.

[Mario Carneiro]

can you reproduce on core lean?

[Jannis Limperg]

I.e. does it segfault when run on the standard library? No, these calls always went through without a hitch.

[Mario Carneiro]

Fixed in lean#752

[Mario Carneiro]

The failing file is algebra/hierarchy_design.lean, which contains some really deep exprs as a result of encoding some huge docstrings as strings

[Jannis Limperg]

That was quick. Thanks!