PatrickMassot / leanblueprint

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

How to generate just a depency graph using xelatex. #51

Closed ouboub closed 5 days ago

ouboub commented 1 week ago

Hi I am on Ubuntu 24.04 (either with tcsh or bash shell) I followed the instructions found in https://leanprover-community.github.io/install/debian.html and https://leanprover-community.github.io/install/project.html

And installed leanprover succesfully I am mainly interested, for the moment, in using blueprint, for my manuscripts, because I want go generate a dependency graph for the proof of theorems, using lemma definition etc. I wish I could use lean for my research, (non linear hyperbolic PDEs), but it seems that Lean, still is not suited for such a task.

So what I have in mind, was for example described in Terence Tao: diagram of papers

Tao mentioned quiver which is nice, but you have to construct most of the graph yourself.

Then there is rdfref But it is a bit buggy, and not that comfortable to use.

So I thought to give blueprint a try, but I run into problem, that I want to report.

Here is what I did

Installation of blueprint

I also followed the instructions How to install blueprint

So in my myproyect folder which is

~/ALLES/HGs/User/Pub/Preprints/Lean/mathematics_in_lean/my_project/my_project 

After running leanblueprint new I have the folder blueprint with a couple of files (I don't understand why \input is used instead of \subfile which allows to run the content.tex file directly) in any case I just wanted to create a dependency graph

So I have

\documentclass[a4paper]{report}
\usepackage{tikz-cd}
\usepackage{geometry}

\usepackage{expl3}
\usepackage[thms=dfn+lem+prop+thm+cor]{blueprint}
\usepackage{amssymb, amsthm, mathtools}
\usepackage[unicode,colorlinks=true,linkcolor=blue,urlcolor=magenta, citecolor=blue]{hyperref}

\usepackage[warnings-off={mathtools-colon,mathtools-overbracket}]{unicode-math}

\input{macros/common}
\input{macros/print}

\title{Energy estimates}
\author{Uwe Brauer}

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

And the content file reads

\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{theorem}[Decaying energy estimate]
  \label{thm:open-ample}
  \lean{sphere_eversion}
  \leanok
  \uses{def:immersion}
  The following estimate holds
\end{theorem}

\begin{proof}
  \leanok
  \uses{thm:open-ample, lem:open_ample_immersion}
  This obviously follows from what we did so far.
\end{proof}

But no graph is generated, what do I miss, or where do I find relevant documentation?

thanks

Uwe Brauer

utensil commented 1 week ago

Option dep_graph is missing from your \usepackage[dep_graph]{blueprint} line.

It should be there if you use the leanblueprint CLI tool to generate your project.

By the way, leanblueprint works perfectly fine without lean. You can use only \label, \uses, and you'll already have your dependency graph. \leanok can be used to mark the state, and it also doesn't involve lean except having lean in its name. If you are not using lean, you don't need to use \lean.

ouboub commented 1 week ago

Option dep_graph is missing from your \usepackage[dep_graph]{blueprint} line.

It should be there if you use the leanblueprint CLI tool to generate your project.

By the way, leanblueprint works perfectly fine without lean. You can use only \label, \uses, and you'll already have your dependency graph. \leanok can be used to mark the state, and it also doesn't involve lean except having lean in its name. If you are not using lean, you don't need to use \lean.

Well it does not work, sorry to say (TL 2004, xelatex) content file reads


\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{theorem}[Decaying energy estimate]
  \label{thm:open-ample}
  \lean{thm:open-ample}
  \leanok
  \uses{def:immersion}
  The following estimate holds
\end{theorem}

\begin{proof}
  \leanok
  \uses{thm:open-ample}
  This obviously follows from what we did so far.
\end{proof}

here is the pdf file print.pdf

utensil commented 1 week ago

Do you have the line like

\usepackage[showmore,dep_graph]{blueprint}

And I guess there is a misunderstanding here, dependency graph is only generated for the web version, see e.g. https://imperialcollegelondon.github.io/FLT/blueprint/dep_graph_chapter_2.html .

However, if you wish to include the same graph in your LaTeX, you can copy the dot code from the source code of the generated html page (right click in the browser and choose view page, then scroll down to almost the bottom), something like:

.renderDot(`strict digraph "" { graph ...lots of stuff .... } `)

  Then you can copy everything between the backtick, and use dot2tex or similar.

It will look like this:

\begin{figure}[H]
    \centering
    {
    \begin{dot2tex}[dot,graphstyle={scale=0.8,transform shape}]
        strict digraph "" { graph ...lots of stuff .... }
    \end{dot2tex}
    }
    \caption{Dependency graph}
    \label{fig:dep_graph}
\end{figure}
ouboub commented 1 week ago

"U" == Utensil @.***> writes:

Do you have the line like

\usepackage[showmore,dep_graph]{blueprint}

No, in your last reply you only mentioned


\usepackage[dep_graph]{blueprint}
``

> And I guess there is a misunderstanding here, dependency graph is only generated for the web version, see e.g.  https://imperialcollegelondon.github.io/FLT/blueprint/dep_graph_chapter_2.html .

Aha, my hope was that it could be used a bit like rdfref, I mentioned in my first message, but appearantly it can't

So if it is not too much to ask, how would I generate the web version (I presume it will only appear on my github repository but not say on a web page running apache on my Laptop)?

> However, if you wish to include the same graph in your LaTeX, you can copy the dot code from the source code of the html page (right click in the browser and choose view page, then scroll down to almost the bottom), something like:

> ```
> .renderDot(`strict digraph "" {   graph ...lots of stuff .... } `)
> ```
>  
> Then you can copy everything between the backtick, and use [dot2tex](https://dot2tex.readthedocs.io/en/latest/) or similar.

Ok dot2tex is what rdfref uses as well.

> It will look like this:

> ```
> \begin{figure}[H]
>     \centering
>     {
>     \begin{dot2tex}[dot,graphstyle={scale=0.8,transform shape}]
>         strict digraph "" {   graph ...lots of stuff .... }
>     \end{dot2tex}
>     }
>     \caption{Dependency graph}
>     \label{fig:dep_graph}
> \end{figure}
> ```

-- 
I strongly condemn Hamas heinous despicable pogroms/atrocities on Israel
I strongly condemn Putin's war of aggression against Ukraine.
I support to deliver weapons to Ukraine's military. 
I support the EU and NATO membership of Ukraine. 
utensil commented 1 week ago

showmore is not required, I just didn't delete all my options.

The webpage is generated and pushed to your Github Pages by Github Actions workflows, as documented in README.

To see them on your own laptop, you don't need apache, just leanblueprint serve which is also mentioned in README.

ouboub commented 1 week ago

leanblueprint serve returned an error of a missing web directory. So I thought, I start again from scratch and I encountered some errors I can't remember to have seen before:

Error: Could not find a Lean project. Please run this command from inside your project folder.

githubactions

You are all set 🎉

but 
`git remote -v`
returns

origin https://github.com/leanprover-community/mathematics_in_lean.git (fetch) origin https://github.com/leanprover-community/mathematics_in_lean.git (push)


Ah, what? I don't want and should not push to his repository, 
what do I miss  here?
ouboub commented 1 week ago

Indeed my first goal is to generate a graph similar to chapter 2 Fermat locally using

So I tried out the exact example of leanbluprint github namely

\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{proof}
  \leanok
  \uses{thm:open_ample, lem:open_ample_immersion}
  This obviously follows from what we did so far.
\end{proof}

and copy this into content.tex then running

Leads to the following display, which I attach,

leanblueprint

but which is not similar to the graph found in chapter 2 Fermat

What do I miss?

Uwe Brauer

utensil commented 1 week ago

Your screenshot isn't complete, on the left panel there should be a chapter with name like dependency graph, and that's where the dep graph is.

ouboub commented 1 week ago

Your screenshot isn't complete, on the left panel there should be a chapter with name like dependency graph, and that's where the dep graph is.

attached you find the complete screenshot, there is no left panel (using the latest chrome browser) (chrome displayed the Fermat example correctly!) leanblueprintcomplete

utensil commented 1 week ago

It's hard to tell which step went wrong without looking at your code. By only descriptions of what you have been piecing things together, I can only make guesses, that's a long shot.

Instead, I would suggest to clone one of the example repos listed in the README, make them work locally, then reduce to what you need.

ouboub commented 1 week ago

ok, that makes sense, shall I clone it into

~/ALLES/HGs/User/Pub/Preprints/Lean/mathematics_in_lean/my_project 

?

utensil commented 1 week ago

Anywhere that doesn't affect your exsiting files should be fine.

ouboub commented 5 days ago

ok, I did, that was helpful thanks