From 066e93ae93913fa4bea7abad41d0a4a9ced38b3a Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 11 Apr 2024 18:00:50 +0200 Subject: [PATCH] some more fixes --- .github/workflows/push.yml | 2 +- README.md | 12 ++++++------ blueprint/src/chapter/main.tex | 2 +- blueprint/src/print.tex | 1 - blueprint/src/web.tex | 9 ++------- 5 files changed, 10 insertions(+), 16 deletions(-) diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index b413c66..56bb6fa 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -18,7 +18,7 @@ jobs: if: always() run: | ! (find BonnAnalysis -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://') -BonnAnalysis + build_project: runs-on: ubuntu-latest name: Build project diff --git a/README.md b/README.md index 8abb9ad..e859f91 100644 --- a/README.md +++ b/README.md @@ -32,17 +32,17 @@ Note: To get this repository, you will need to download Lean's mathematical libr * Open a terminal (I recommend `git bash` on Windows, which was installed as part of git in the first step). -* Use `cd` to navigate to a directory where you would like to create the `LeanInRome` folder. +* Use `cd` to navigate to a directory where you would like to create the `BonnAnalysis` folder. -* Run `git clone https://github.com/fpvandoorn/LeanInRome.git`. +* Run `git clone https://github.com/fpvandoorn/BonnAnalysis.git`. -* Run `cd LeanInRome` +* Run `cd BonnAnalysis` * Run `lake exe cache get!` * This downloads mathlib, and will take a bit of time * On Windows, if you get an error that starts with `curl: (35) schannel: next InitializeSecurityContext failed` it is probably your antivirus program that doesn't like that we're downloading many files. The easiest solution is to temporarily disable your antivirus program. -* Run `lake build +LeanInRome.Common` +* Run `lake build +BonnAnalysis.Common` * This should take less than 1 minute. If you get more than a few lines of output, then you're rebuilding Mathlib from scratch, which means that the previous step went wrong. You can quit the execution and ask for help. * Launch VS Code, either through your application menu or by typing @@ -52,7 +52,7 @@ Note: To get this repository, you will need to download Lean's mathematical libr * If you launched VS Code from a menu, on the main screen, or in the File menu, click "Open folder" (just "Open" on a Mac), and choose the folder - `LeanInRome` (*not* one of its subfolders). + `BonnAnalysis` (*not* one of its subfolders). -* Test that everything is working by opening `LeanInRome/Test.lean`. +* Test that everything is working by opening `BonnAnalysis/Test.lean`. It is normal if it takes 10-60 seconds for Lean to start up. \ No newline at end of file diff --git a/blueprint/src/chapter/main.tex b/blueprint/src/chapter/main.tex index 8a19131..8dca0a6 100644 --- a/blueprint/src/chapter/main.tex +++ b/blueprint/src/chapter/main.tex @@ -4,7 +4,7 @@ \title{Blueprint for the collaborative Formalization Seminar} -\author{participants to the formalization seminar} +\author{} \maketitle diff --git a/blueprint/src/print.tex b/blueprint/src/print.tex index c5db4c4..3d30ada 100644 --- a/blueprint/src/print.tex +++ b/blueprint/src/print.tex @@ -32,6 +32,5 @@ \input{preamble/print} \begin{document} -\maketitle \input{chapter/main} \end{document} diff --git a/blueprint/src/web.tex b/blueprint/src/web.tex index c293ef9..a27fcd7 100644 --- a/blueprint/src/web.tex +++ b/blueprint/src/web.tex @@ -16,14 +16,9 @@ \input{preamble/common} \input{preamble/web} -%\home{https://github.com/teorth/pfr/} -\github{https://github.com/teorth/pfr/} -\dochome{https://teorth.github.io/pfr/docs} - -\title{PFR} -\author{} +\github{https://github.com/fpvandoorn/BonnAnalysis} +\dochome{https://fpvandoorn.github.io/BonnAnalysis/docs} \begin{document} -\maketitle \input{chapter/main} \end{document}