PatrickMassot / leanblueprint

plasTeX plugin to build formalization blueprints.
Apache License 2.0
163 stars 26 forks source link

leanblueprint web fails with error. (python 3.12, ubuntu 24.04) #53

Closed ouboub closed 5 days ago

ouboub commented 1 week ago

Hi I hopefully managed to setup leanblueprint See my environment I have the following content file

\begin{definition}[Immersion]
\label{def:immersion}
  The following 
\end{definition}

\begin{theorem}[Smale 1958]
  \label{thm:sphere_eversion}
  \lean{sphere_eversion}
  \leanok
  \uses{def:immersion}
  There is a homotopy of immersions of $𝕊^2$ into $ℝ^3$ from the inclusion map to
  the antipodal map $a : q ↦ -q$.
\end{theorem}

\begin{lemma}[Decaying estimate]
\label{lem:decay}
  The following 
\end{lemma}

\begin{proof}
  \leanok
  \uses{thm:sphere_eversion, lem:decay}
  This obviously follows from what we did so far.
\end{proof}

and web.tex

\documentclass{report}

\usepackage{amssymb, amsthm, amsmath}
\usepackage{hyperref}
\usepackage[showmore, dep_graph]{blueprint}

\input{macros/common}
\input{macros/web}

\home{https://github.com/ouboub/Lean-Euler-Nordstroem}
\github{https://github.com/ouboub/Lean-Euler-Nordstroem}
\dochome{https://github.com/ouboub/Lean-Euler-Nordstroem}

\title{Global existence}
\author{Uwe Brauer}

\begin{document}
\maketitle
\input{content}
\end{document}

print.tex looks similar leanblueprint pdf works but leandprint web returns

)
 (loading package /home/oub/.local/lib/python3.12/site-
   packages/plastexshowmore/Packages/showmore.py
 ) ).. ( ./macros/common.tex ).... ( ./macros/web.tex )......
 ( ./content.tex )....Traceback (most recent call last):
  File "/home/oub/.local/bin/plastex", line 8, in <module>
    sys.exit(plastex())
             ^^^^^^^^^
  File "/home/oub/.local/lib/python3.12/site-packages/plasTeX/client.py", line 72, in plastex
    main(sys.argv[1:])
  File "/home/oub/.local/lib/python3.12/site-packages/plasTeX/client.py", line 52, in main
    run(filename, config)
  File "/home/oub/.local/lib/python3.12/site-packages/plasTeX/Compile.py", line 90, in run
    tex = parse(filename, config)
          ^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/oub/.local/lib/python3.12/site-packages/plasTeX/Compile.py", line 85, in parse
    tex.parse()
  File "/home/oub/.local/lib/python3.12/site-packages/plasTeX/TeX.py", line 428, in parse
    callback()
  File "/home/oub/.local/lib/python3.12/site-packages/leanblueprint/Packages/blueprint.py", line 233, in make_lean_data
    n) == 'definition' for n in graph.ancestors(node).union({node}))
                                ^^^^^^^^^^^^^^^^^^^^^
  File "/home/oub/.local/lib/python3.12/site-packages/plastexdepgraph/Packages/depgraph.py", line 112, in ancestors
    pred.union(*map(self.ancestors, pred)))
    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/oub/.local/lib/python3.12/site-packages/plastexdepgraph/Packages/depgraph.py", line 112, in ancestors
    pred.union(*map(self.ancestors, pred)))
    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/oub/.local/lib/python3.12/site-packages/plastexdepgraph/Packages/depgraph.py", line 112, in ancestors
    pred.union(*map(self.ancestors, pred)))
    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  [Previous line repeated 988 more times]
  File "/home/oub/.local/lib/python3.12/site-packages/plastexdepgraph/Packages/depgraph.py", line 110, in ancestors
    pred = self.predecessors(node)
           ^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/oub/.local/lib/python3.12/site-packages/plastexdepgraph/Packages/depgraph.py", line 94, in predecessors
    if node in self._predecessors:
       ^^^^^^^^^^^^^^^^^^^^^^^^^^
RecursionError: maximum recursion depth exceeded
Command 'plastex -c plastex.cfg web.tex' returned non-zero exit status 1.

that looks like a Bug with python3.12?

utensil commented 1 week ago

It causes infinite recursion because you used lemma decay in the proof of lemma decay.

ouboub commented 5 days ago

ok, understood