blueprint

Stream: condensed mathematics

[Adam Topaz]

What's the preferred workflow for editing the blueprint latex files locally? Seems that I must use xelatex to compile a pdf file?

[Patrick Massot]

There is no mystery here, invoke is simply doing this

[Yakov Pechersky]

If you want to configure your machine similar to how the CI does it, you can look at https://github.com/leanprover-community/liquid/blob/master/.github/workflows/gh-pages.yml

[Adam Topaz]

Thanks. My main issue is that I have emacs set up to run latexmk and I don't know how to make this compatible with xelatex

[Adam Topaz]

but it looks like editing my .latexmkrc file per
https://stackoverflow.com/questions/3124273/compile-xelatex-tex-file-with-latexmk
should do the trick

[Mauricio Collares]

$pdf_mode = 5; in .latexmkrc should do the trick

[Johan Commelin]

I am trying to build the blueprint for this PR: https://github.com/leanprover-community/liquid/pull/8
But I get a segfault when trying to list the decls.

lean --run src/list_decls.lean
Segmentation fault (core dumped)

cc @Patrick Massot @Mario Carneiro

[Mario Carneiro]

where is the list_decls.lean file? There are some environment listing functions that cause a stack overflow because of the creation of a list declaration, either directly or internally

[Johan Commelin]

It is generated by the blueprint software

[Johan Commelin]

I pushed a copy to the list-decls branch

[Mario Carneiro]

https://github.com/leanprover-community/liquid/tree/list-decls ?

[Mauricio Collares]

https://github.com/leanprover-community/lean-liquid/tree/list-decls

[Johan Commelin]

Does this require stepping through Lean in gdb? I think Reid once showed me how to do that, but I forgot all about it. That was > 2 yrs ago or so.

[Mauricio Collares]

Looks like very deep but not infinite recursion, because it works if I do ulimit -s unlimited before running Lean. With a small stack (and therefore probably corrupted top frames), the backtrace is:

#0  0x0000000000f06caa in std::__uninitialized_copy<false>::__uninit_copy<lean::vm_obj const*, lean::vm_obj*> (__first=<error reading variable: Cannot access memory at address 0x7fffff7fefe8>, __last=<error reading variable: Cannot access memory at address 0x7fffff7fefe0>,
    __result=<error reading variable: Cannot access memory at address 0x7fffff7fefd8>) at /nix/store/dwnrcww53x9vay3w16pwbyy3g666736x-gcc-11.3.0/include/c++/11.3.0/bits/stl_uninitialized.h:85
#1  0x0000000000f01d2f in std::uninitialized_copy<lean::vm_obj const*, lean::vm_obj*> (__first=0x7fffff7ff160, __last=0x7fffff7ff170, __result=0xb0da9040) at /nix/store/dwnrcww53x9vay3w16pwbyy3g666736x-gcc-11.3.0/include/c++/11.3.0/bits/stl_uninitialized.h:151
#2  0x0000000000ed5278 in lean::vm_composite::vm_composite (this=0xb0da9030, k=lean::vm_obj_kind::Constructor, idx=1, sz=2, data=0x7fffff7ff160) at /home/collares/lean/src/library/vm/vm.cpp:65
#3  0x0000000000ed5339 in lean::mk_vm_composite (k=lean::vm_obj_kind::Constructor, idx=1, sz=2, data=0x7fffff7ff160) at /home/collares/lean/src/library/vm/vm.cpp:70
#4  0x0000000000ed54a4 in lean::mk_vm_constructor (cidx=1, sz=2, data=0x7fffff7ff160) at /home/collares/lean/src/library/vm/vm.cpp:87
#5  0x0000000000f2dba1 in lean::string_to_list_core (str=..., reverse=false) at /home/collares/lean/src/library/vm/vm_string.cpp:112
#6  0x0000000000f2dd1d in lean::string_to_list (s=...) at /home/collares/lean/src/library/vm/vm_string.cpp:118
#7  0x0000000000edea5b in lean::vm_state::invoke_fn (this=0x7fffffffac40, fn=0xf2dcda <lean::string_to_list(lean::vm_obj const&)>, arity=1) at /home/collares/lean/src/library/vm/vm.cpp:1786
#8  0x0000000000ef4047 in lean::vm_state::invoke_cfun (this=0x7fffffffac40, d=...) at /home/collares/lean/src/library/vm/vm.cpp:3032
#9  0x0000000000ef6795 in lean::vm_state::run (this=0x7fffffffac40) at /home/collares/lean/src/library/vm/vm.cpp:3566
#10 0x0000000000edffed in lean::vm_state::invoke_closure (this=0x7fffffffac40, fn=..., nargs=1) at /home/collares/lean/src/library/vm/vm.cpp:1870
#11 0x0000000000ee360d in lean::vm_state::invoke (this=0x7fffffffac40, fn=..., a1=...) at /home/collares/lean/src/library/vm/vm.cpp:1945
#12 0x0000000000ee5dda in lean::vm_state::invoke (this=0x7fffffffac40, fn=..., a1=..., a2=...) at /home/collares/lean/src/library/vm/vm.cpp:1987#22532 0x0000000000eee997 in lean::invoke (fn=..., a1=..., a2=...) at /home/collares/lean/src/library/vm/vm.cpp:2439
...[omitted frames are just lots of copies of the five frames below]...
#22533 0x0000000000f38f53 in lean::io_bind (a=..., b=...) at /home/collares/lean/src/library/vm/vm_io.cpp:745
#22534 0x0000000000eef84b in lean::native_invoke (fn=..., a1=...) at /home/collares/lean/src/library/vm/vm.cpp:2569
#22535 0x0000000000eee845 in lean::invoke (fn=..., a1=...) at /home/collares/lean/src/library/vm/vm.cpp:2427
#22536 0x0000000000ee5dfa in lean::vm_state::invoke (this=0x7fffffffac40, fn=..., a1=..., a2=...) at /home/collares/lean/src/library/vm/vm.cpp:1987
#22537 0x0000000000eee997 in lean::invoke (fn=..., a1=..., a2=...) at /home/collares/lean/src/library/vm/vm.cpp:2439
#22538 0x0000000000f38f53 in lean::io_bind (a=..., b=...) at /home/collares/lean/src/library/vm/vm_io.cpp:745
#22539 0x0000000000edefaf in lean::vm_state::invoke_fn (this=0x7fffffffac40, fn=0xf38c99 <lean::io_bind(lean::vm_obj const&, lean::vm_obj const&, lean::vm_obj const&, lean::vm_obj const&, lean::vm_obj const&)>, arity=5) at /home/collares/lean/src/library/vm/vm.cpp:1810
#22540 0x0000000000ef6003 in lean::vm_state::run (this=0x7fffffffac40) at /home/collares/lean/src/library/vm/vm.cpp:3464
#22541 0x0000000000ef71af in lean::vm_state::execute (this=0x7fffffffac40, code=0x7fffffff92e0) at /home/collares/lean/src/library/vm/vm.cpp:3617
#22542 0x0000000000ef729c in lean::vm_state::apply (this=0x7fffffffac40, n=1) at /home/collares/lean/src/library/vm/vm.cpp:3625
#22543 0x0000000000ee031f in lean::vm_state::invoke (this=0x7fffffffac40, fn_idx=45326, nargs=1, as=0x7fffffffabc0) at /home/collares/lean/src/library/vm/vm.cpp:1901
#22544 0x0000000000ee0449 in lean::vm_state::invoke (this=0x7fffffffac40, fn='main', nargs=1, as=0x7fffffffabc0) at /home/collares/lean/src/library/vm/vm.cpp:1910
#22545 0x0000000000e2bedb in lean::eval_helper::invoke_fn (this=0x7fffffffa6c0) at /home/collares/lean/src/library/eval_helper.cpp:38
#22546 0x0000000000e2c000 in lean::eval_helper::try_exec_io (this=0x7fffffffa6c0) at /home/collares/lean/src/library/eval_helper.cpp:44
#22547 0x0000000000e2c52b in lean::eval_helper::try_exec (this=0x7fffffffa6c0) at /home/collares/lean/src/library/eval_helper.cpp:73
#22548 0x0000000000c6f9f4 in main (argc=3, argv=0x7fffffffaf18) at /home/collares/lean/src/shell/lean.cpp:674

[Mauricio Collares]

I guess the script uses a bunch of non-tail-recursive functions (list.{filter,split,mmap'}) on a large list (decls)

[Johan Commelin]

Does this suggest a solution to the script? Or should we just do that ulimit unlimited thing in CI?

[Mauricio Collares]

To be honest, I don't know. I tried replacing main by

meta def main : io unit :=
do curr_env ← run_tactic get_env,
   h ← mk_file_handle "decls.yaml" mode.write,
   let decls := curr_env.fold [] (λ x l, if not (to_name x).is_internal then (x :: l) else l),
   decls.mfoldl (λ _ d, (print_item_crawl curr_env h d)) (),
   close h

which seems to only use tail-recursive functions up to the binds inside mfoldl, but I still get a segfault (which goes away if I comment the next-to-last line). So I don't understand how Lean's runtime executes IO actions enough to fix the code.

[Ben Toner]

I'm a fan of Mauricio's ulimit -s unlimited "solution", noting that the problem will come back for real (process will run out of memory; no easy fixes then) at some point if the project gets bigger -- but I'd expect it to need to get quite a bit bigger before this happens and probably it never gets there. This assumes the stack size in linear in the number of definitions; if it's quadratic, this solution may not buy much time at all (but why would a list-decls script be doing something quadratic?) #fix-it-in-lean4

[Mauricio Collares]

The default stack size on Linux is pretty small (8MB), even ulimit -s 1048576 to bump it to 1GB would be a gigantic increase

[Ben Toner]

I didn't know that -- well now I'm an even bigger fan of bumping the stack size, since the project would have to become ginormous for the stack to not fit in memory.

[Johan Commelin]

Is it easy to change the ulimit in CI?

[Johan Commelin]

(If either of you needs access to the blueprint repo, just ping me.)

[Mauricio Collares]

Let's see if the naive solution works: https://github.com/leanprover-community/liquid/pull/11

[Johan Commelin]

Thanks! Seems to have worked!

[Johan Commelin]

Can we also run deploys on PR branches somehow?

[Ben Toner]

Johan Commelin said:

Can we also run deploys on PR branches somehow?

https://github.com/leanprover-community/liquid/pull/12

Let me know if this behaviour works for you.

[Filippo A. E. Nuccio]

In the Introduction the main theorem is a theoremxrather than a theorem. Since theoremxis in particular a newtheorem*, it does not get numbered and the reference at the end of the first paragraph below the Main Theorem sends to 0.0.2 (which is the definition of $\mathbb{N}$). I hesitate to open a PR, because changing theoremxto theorem would probably insert it in the dependency graph.

[Johan Commelin]

Sorry, I forgot about this one. I'll fix it tonight.

[Johan Commelin]

I pushed a fix, it should be live soon

[Johan Commelin]

CI isn't kicking in... does someone know why?

[Adam Topaz]

sometimes GitHub shuts down ci after 6mo (I think) of inactivity. Is this the issue?

[Johan Commelin]

possibly or even probably...
can we reactivite it?

[Adam Topaz]

Can you run the ci manually? It may just work

[Johan Commelin]

I just tried something... let's see if it helps

[Johan Commelin]

doesn't seem to have worked

[Johan Commelin]

I want to PR some clean-ups to the lean-liquid repo. But that requires updating the blueprint, to keep it in sync.

[Johan Commelin]

However, CI on the blueprint repo seems to have died, and I have no idea how to revive it.

[Johan Commelin]

If someone wants to help with that, I would be very grateful.

[Johan Commelin]

For example, here is a PR that renames exact_with_constant to strongly_exact:
https://github.com/leanprover-community/lean-liquid/pull/130

[Johan Commelin]

And here is the companion PR to the blueprint repo:
https://github.com/leanprover-community/liquid/pull/16

[Yaël Dillies]

Restarting CI is very easy. You can go to the workflow page on the repo. If nobody beats me to it, I'll do so in an hour

[Johan Commelin]

I already tried that

[Mauricio Collares]

cc @Wojciech Nawrocki since I think runs-on: liquid means it relates to a Hoskinson runner

[Mauricio Collares]

But this relates to the first PR only. The second PR is stalled just because ubuntu-18.04 is deprecated: https://github.com/leanprover-community/liquid/pull/17

[Johan Commelin]

Thanks, merged

[Mauricio Collares]

The current blueprint error (second PR listed above) is this:

| [imager] INFO: This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live
|    2023) (preloaded format=latex)
| [imager] INFO: restricted \write18 enabled.
| [imager] INFO: entering extended mode
| [imager] INFO: (./images-ym2zcxxx.tex
| [imager] INFO: LaTeX2e <2023-06-01> patch level 1
| [imager] INFO: L3 programming layer <2023-06-16>
| [imager] INFO:
| [imager] INFO: (/opt/texlive/texdir/texmf-dist/tex/latex/base/article.cls
| [imager] INFO: Document Class: article 2023/05/17 v1.4n Standard LaTeX
|    document class
| [imager] INFO: (/opt/texlive/texdir/texmf-dist/tex/latex/base/size10.clo))
| [imager] INFO:
| [imager] INFO: ! LaTeX Error: File `blueprint.sty' not found.
| [imager] INFO:
| [imager] INFO: Type X to quit or <RETURN> to proceed,
| [imager] INFO: or enter new name. (Default extension: sty)
| [imager] INFO:
| [imager] INFO: Enter file name:
| [imager] INFO: ! Emergency stop.
| [imager] INFO: <read *>
| [imager] INFO:
| [imager] INFO: l.5 ^^M
| [imager] INFO:
| [imager] INFO: No pages of output.
| [imager] INFO: Transcript written on images-ym2zcxxx.log.
| WARNING: Failed to compile image: Command 'latex images-ym2zcxxx.tex'
|    returned non-zero exit status 1.
| WARNING: Source files are saved at /tmp/tmp6z1vkmf7.

[Mauricio Collares]

This changed in plastex commit https://github.com/plastex/plastex/commit/ac0369937d8e011c8191484b26a1825f45481bdc. You can see the liquid blueprint logs before and after the plastex change in https://github.com/collares/liquid/actions/runs/5561140520/jobs/10158610045 and https://github.com/collares/liquid/actions/runs/5561141722/jobs/10158612139 respectively. cc @Patrick Massot

[Wojciech Nawrocki]

Mauricio Collares said:

cc Wojciech Nawrocki since I think runs-on: liquid means it relates to a Hoskinson runner

It doesn't seem to be running on hoskinson, e.g. this run was on a Github Actions-hosted machine. But in any case the error you saw here shouldn't vary per runner as it is an actual problem with building the blueprint.

[Wojciech Nawrocki]

@Mauricio Collares where did you see the runs-on: liquid? Those jobs should run on CI runners labeled with liquid, except that there are no such runners.

[Wojciech Nawrocki]

Oh I see, it was on the lean-liquid/ repo rather than liquid/. I added the label to one runner so that lean-liquid#130 could run. GitHub automatically removes labels that hadn't been used for a while, and it looks like last CI activity with the liquid label was back in 2022.

[Mauricio Collares]

Thank you, and sorry for the confusing ping!

[Mauricio Collares]

https://github.com/plastex/plastex/pull/339 for the blueprint issue

[Johan Commelin]

cc @Patrick Massot

[Johan Commelin]

@Mauricio Collares thanks for digging into this!

[Patrick Massot]

I'll take a look. I'm curious, why is this blueprint moving now?

[Johan Commelin]

Johan Commelin said:

I want to PR some clean-ups to the lean-liquid repo. But that requires updating the blueprint, to keep it in sync.

@Patrick Massot :up:

[Johan Commelin]

Patrick managed to get CI working again!

[Johan Commelin]

I just merged a little bit of polish into the blueprint repo