Try better config

Author: jcreedcmu

.github/workflows/blueprint.yml

@@ -37,6 +37,6 @@ jobs:
         uses: jcreedcmu/docgen-action@main
         with:
           lake-package-directory: inner_directory
-          blueprint: true
           homepage: inner_directory/home_page
+          blueprint: true
           api-docs: true

.gitignore

@@ -1 +1,15 @@
 /inner_directory/.lake
+inner_directory/blueprint/print
+inner_directory/blueprint/web
+inner_directory/blueprint/src/web.paux
+inner_directory/blueprint/src/web.bbl
+inner_directory/blueprint/lean_decls
+texput.log
+
+# These are created if you manually run tex in blueprint/src
+inner_directory/blueprint/src/print.aux
+inner_directory/blueprint/src/print.bbl
+inner_directory/blueprint/src/print.blg
+inner_directory/blueprint/src/print.log
+inner_directory/blueprint/src/print.out
+inner_directory/blueprint/src/print.pdf

inner_directory/BlueprintDebug.lean

@@ -1,3 +1,10 @@
--- This module serves as the root of the `BlueprintDebug` library.
--- Import modules here that should be built as part of the library.
+import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
 import BlueprintDebug.Basic
+
+open Real
+
+/--
+Some docstring for this guy
+-/
+noncomputable
+def foobar := 123 + π

inner_directory/blueprint/src/content.tex

@@ -4,4 +4,9 @@
 %
 % If you want to split the blueprint content into several files then
 % the current file can be a simple sequence of \input. Otherwise It
-% can start with a \section or \chapter for instance.
+% can start with a \section or \chapter for instance.
+
+\begin{definition}
+Define {\em foobar} to be $123 + \pi$.
+\lean{foobar}
+\end{definition}