bump blueprint

.github/workflows/build.yaml → .github/workflows/build_blueprint.yml

@@ -16,15 +16,17 @@ jobs:
         with:
           extra-conf: |
             accept-flake-config = true
-      #- uses: DeterminateSystems/magic-nix-cache-action@main
+      - uses: DeterminateSystems/magic-nix-cache-action@main
       - uses: DeterminateSystems/flake-checker-action@main
       - name: Checkout Project
         uses: actions/checkout@v3
         with:
           fetch-depth: 2
           lfs: true
+
       - run: |
           nix develop --command make blueprint
+
       - name: Fix permissions
         run: |
           chmod -c -R +rX "blueprint/web/" | while read line; do
@@ -37,4 +39,4 @@ jobs:
           path: blueprint/web/
       - name: Deploy to GitHub Pages
         id: deployment
-        uses: actions/deploy-pages@v1
+        uses: actions/deploy-pages@v1

.github/workflows/build_project.yml

@@ -0,0 +1,35 @@
+name: Build project
+run-name: Build project
+on:
+  workflow_dispatch:
+  pull_request:
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          ./elan-init -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - uses: actions/checkout@v4
+
+      - name: print lean and lake versions
+        run: |
+          lean --version
+          lake --version
+
+      - name: get mathlib cache
+        continue-on-error: true
+        run: |
+          lake exe cache clean
+          # We've been seeing many failures at this step recently because of network errors.
+          # As a band-aid, we try twice.
+          # The 'sleep 1' is small pause to let the network recover.
+          lake exe cache get || (sleep 1; lake exe cache get)
+
+      - name: building
+        run: lake build

Makefile

@@ -2,25 +2,29 @@
 
 PROJECT = RamificationGroup
 
-.PHONY: all build blueprint blueprint-dev analyze serve update
+.PHONY: all build blueprint blueprint-dev analyze
 
 all : build blueprint
 
 build:
-	(lake -Kenv=dev exe cache get && lake -Kenv=dev build && lake -Kenv=dev build ${PROJECT}:docs)
+	(lake exe cache get && lake build)
 
-blueprint: build
-	(cd blueprint && inv all && cp -r ../.lake/build/doc ./web/)
+build-print:
+	(cd blueprint && mkdir -p print && cd src && xelatex -output-directory=../print print.tex)
+	(cd blueprint/print && BIBINPUTS=../src bibtex print.aux)
+	(cd blueprint/src && xelatex -output-directory=../print print.tex)
+	(cd blueprint/src && xelatex -output-directory=../print print.tex)
+	(cp blueprint/print/print.bbl blueprint/src/web.bbl)
 
-blueprint-dev:
-	(cd blueprint && inv all)
+build-web:
+	(cd blueprint/src && poetry run plastex -c plastex.cfg web.tex)
 
-analyze:
-	(python3 blueprint/blueprint_auto.py -p ${PROJECT})
+blueprint: build build-print build-web
+	(lake -Kenv=dev update doc-gen4 && lake -Kenv=dev build $(PROJECT):docs)
+	(cd blueprint && cp -r ../.lake/build/doc ./web/)
 
-serve: blueprint-dev analyze
-	(cd blueprint && inv serve)
+blueprint-dev: build-print build-web
+	(cd blueprint/web && poetry run python -m http.server)
 
-update:
-	(curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain && \
-		lake -Kenv=dev update -R)
+analyze:
+	(poetry run python3 blueprint/blueprint_auto.py -p ${PROJECT})

pyproject.toml

@@ -0,0 +1,16 @@
+[tool.poetry]
+name = "blueprint-template"
+version = "0.1.0"
+description = ""
+authors = ["timechess <tyc221@ruc.edu.cn>"]
+readme = "README.md"
+
+[tool.poetry.dependencies]
+python = "^3.11"
+watchfiles = "^0.23.0"
+plastex = "^3.1"
+leanblueprint = "^0.0.14"
+
+[build-system]
+requires = ["poetry-core"]
+build-backend = "poetry.core.masonry.api"

shell.nix

@@ -1,38 +1,14 @@
 { pkgs, ... }:
 let
-   pythonPackages = pkgs.python39Packages;
-   tex = (pkgs.texlive.combine {
-     inherit (pkgs.texlive)
-       scheme-small dvisvgm
-       amsmath hyperref comment;
-   });
+  tex = (pkgs.texlive.combine {
+    inherit (pkgs.texlive)
+      scheme-small dvisvgm
+      amsmath hyperref comment;
+  });
 in pkgs.mkShell {
-  name = "python-venv";
-  venvDir = "./.venv";
+  packages = with pkgs; [ tex graphviz pdf2svg elan gnumake poetry ];
 
-  packages = with pkgs; [ tex graphviz pdf2svg elan gnumake ];
-
-  buildInputs = [
-    # A Python interpreter including the 'venv' module is required to bootstrap
-    # the environment.
-    pythonPackages.python
-
-    # This executes some shell code to initialize a venv in $venvDir before
-    # dropping into the shell
-    pythonPackages.venvShellHook
-
-  ];
-
-  # Run this command, only after creating the virtual environment
-  postVenvCreation = ''
-    unset SOURCE_DATE_EPOCH
-    pip install -r requirements.txt
-  '';
-
-  # Now we can execute any commands within the virtual environment.
-  # This is optional and can be left out to run pip manually.
-  postShellHook = ''
-    # allow pip to install wheels
-    unset SOURCE_DATE_EPOCH
+  shellHook = ''
+    poetry install
   '';
 }