From 1f22de24da72e8d4e8603b477eca1729e42c0d59 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?SnO=E2=82=82WMaN?= Date: Tue, 15 Oct 2024 12:41:39 +0900 Subject: [PATCH] refactor/ci: rename package name and fix (#5) --- .github/workflows/ci.yml | 79 +------------------ Arithmetization/Definability/Hierarchy.lean | 2 +- .../ISigmaOne/Metamath/CodedTheory.lean | 2 +- .../ISigmaOne/Metamath/Proof/Typed.lean | 2 +- Arithmetization/Vorspiel/Vorspiel.lean | 4 +- lake-manifest.json | 56 ++----------- lakefile.lean | 14 +--- 7 files changed, 17 insertions(+), 142 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 09e9870..6f4953f 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1,7 +1,5 @@ name: CI -# https://github.com/FormalizedFormalLogic/Foundation/blob/master/.github/workflows/ci.yml - on: push: branches: @@ -9,11 +7,6 @@ on: pull_request: workflow_dispatch: -permissions: - contents: read - pages: write - id-token: write - concurrency: group: ${{ github.workflow }}-${{ github.ref }} cancel-in-progress: true @@ -24,74 +17,4 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 - - name: Install elan - run: | - curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none - echo "$HOME/.elan/bin" >> $GITHUB_PATH - - name: Check toolchain version - run: | - elan --version - lake --version - lean --version - - uses: actions/cache@v4 - with: - path: .lake - key: lake-${{ runner.os }}-${{ hashFiles('lean-toolchain') }} - restore-keys: lake-${{ runner.os }}-${{ hashFiles('lean-toolchain') }} - - - name: Fetching cache - run: lake -R -Kenv=ci exe cache get - - - name: Build project - run: lake -R -Kenv=ci build - - - uses: ts-graphviz/setup-graphviz@v2 - - name: Generate import graph - run: | - lake -R -Kenv=ci exe graph - dot -Tpng ./import_graph.dot -o import_graph.png - dot -Tpdf ./import_graph.dot -o import_graph.pdf - - name: Upload import graph - uses: actions/upload-artifact@v4 - if: github.ref == 'refs/heads/master' - with: - name: import_graph - path: | - ./import_graph.dot - ./import_graph.png - ./import_graph.pdf - - # Generate document only master branch - - name: Generate document - if: github.ref == 'refs/heads/master' - run: lake -R -Kenv=ci build Logic:docs Arithmetization:docs - - name: Upload document - uses: actions/upload-artifact@v4 - if: github.ref == 'refs/heads/master' - with: - name: docs - path: ./.lake/build/doc - - deploy: - name: Deploy to GitHub Pages - runs-on: ubuntu-latest - if: github.ref == 'refs/heads/master' - environment: - name: github-pages - url: ${{ steps.deployment.outputs.page_url }} - needs: - - build - steps: - - uses: actions/download-artifact@v4 - with: - name: docs - path: ./_site/docs/ - - uses: actions/download-artifact@v4 - with: - name: import_graph - path: ./_site/assets/import_graph/ - - uses: actions/upload-pages-artifact@v3 - with: - path: ./_site - - uses: actions/deploy-pages@v4 - id: deployment \ No newline at end of file + - uses: leanprover/lean-action@v1 \ No newline at end of file diff --git a/Arithmetization/Definability/Hierarchy.lean b/Arithmetization/Definability/Hierarchy.lean index 1fd163c..926d919 100644 --- a/Arithmetization/Definability/Hierarchy.lean +++ b/Arithmetization/Definability/Hierarchy.lean @@ -1,5 +1,5 @@ import Arithmetization.Vorspiel.Lemmata -import Logic.FirstOrder.Arith.StrictHierarchy +import Foundation.FirstOrder.Arith.StrictHierarchy /-! diff --git a/Arithmetization/ISigmaOne/Metamath/CodedTheory.lean b/Arithmetization/ISigmaOne/Metamath/CodedTheory.lean index f065a1d..fad8a7a 100644 --- a/Arithmetization/ISigmaOne/Metamath/CodedTheory.lean +++ b/Arithmetization/ISigmaOne/Metamath/CodedTheory.lean @@ -1,6 +1,6 @@ import Arithmetization.ISigmaOne.Metamath.Coding import Arithmetization.ISigmaOne.Metamath.Proof.Typed -import Logic.FirstOrder.Arith.PeanoMinus +import Foundation.FirstOrder.Arith.PeanoMinus namespace LO.FirstOrder.Semiformula diff --git a/Arithmetization/ISigmaOne/Metamath/Proof/Typed.lean b/Arithmetization/ISigmaOne/Metamath/Proof/Typed.lean index 3d1497f..6f0fb50 100644 --- a/Arithmetization/ISigmaOne/Metamath/Proof/Typed.lean +++ b/Arithmetization/ISigmaOne/Metamath/Proof/Typed.lean @@ -1,6 +1,6 @@ import Arithmetization.ISigmaOne.Metamath.Formula.Typed import Arithmetization.ISigmaOne.Metamath.Proof.Derivation -import Logic.Logic.HilbertStyle.Supplemental +import Foundation.Logic.HilbertStyle.Supplemental /-! diff --git a/Arithmetization/Vorspiel/Vorspiel.lean b/Arithmetization/Vorspiel/Vorspiel.lean index a9e5f55..329a33e 100644 --- a/Arithmetization/Vorspiel/Vorspiel.lean +++ b/Arithmetization/Vorspiel/Vorspiel.lean @@ -1,5 +1,5 @@ -import Logic.FirstOrder.Arith.Representation -import Logic.FirstOrder.Arith.PeanoMinus +import Foundation.FirstOrder.Arith.Representation +import Foundation.FirstOrder.Arith.PeanoMinus instance [Zero α] : Nonempty α := ⟨0⟩ diff --git a/lake-manifest.json b/lake-manifest.json index 256bce0..821e27b 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -34,12 +34,12 @@ {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "scope": "", - "rev": "bf1a80e92be21e3562dd618b95cc24b57a6d476a", + "scope": "leanprover-community", + "rev": "d1b33202c3a29a079f292de65ea438648123b635", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "v0.0.39", - "inherited": false, + "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", @@ -59,7 +59,7 @@ "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7", - "inherited": false, + "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", @@ -68,57 +68,17 @@ "rev": "ab9dec5b351bc7e92f30b47031edf13458bc7a1d", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": null, + "inputRev": "ab9dec5b351bc7e92f30b47031edf13458bc7a1d", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/FormalizedFormalLogic/Foundation", "type": "git", "subDir": null, "scope": "", - "rev": "c14a269c27ee9ef7936bcbb84fc7c51056480479", - "name": "logic", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/acmepjz/md4lean", - "type": "git", - "subDir": null, - "scope": "", - "rev": "9148a0a7506099963925cf239c491fcda5ed0044", - "name": "MD4Lean", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/fgdorais/lean4-unicode-basic", - "type": "git", - "subDir": null, - "scope": "", - "rev": "f93115d0209de6db335725dee900d379f40c0317", - "name": "UnicodeBasic", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/dupuisf/BibtexQuery", - "type": "git", - "subDir": null, - "scope": "", - "rev": "bd8747df9ee72fca365efa5bd3bd0d8dcd083b9f", - "name": "BibtexQuery", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/doc-gen4", - "type": "git", - "subDir": null, - "scope": "", - "rev": "b941c425f6f0f1dc45fe13b850ffa7db1bb20d04", - "name": "«doc-gen4»", + "rev": "10cdf9cf9d88117471d50a526b64e56b802714f3", + "name": "foundation", "manifestFile": "lake-manifest.json", - "inputRev": "b941c425f6f0f1dc45fe13b850ffa7db1bb20d04", + "inputRev": "rename", "inherited": false, "configFile": "lakefile.lean"}], "name": "arithmetization", diff --git a/lakefile.lean b/lakefile.lean index 61d9da2..fb6654f 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -1,21 +1,13 @@ import Lake open Lake DSL -package «arithmetization» { +package arithmetization { -- add any package configuration options here } @[default_target] -lean_lib «Arithmetization» { +lean_lib Arithmetization { -- add any library configuration options here } -require logic from git "https://github.com/FormalizedFormalLogic/Foundation" @ "master" - -require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4"@"v0.0.39" - -meta if get_config? env = some "ci" then -require importGraph from git "https://github.com/leanprover-community/import-graph" @ "68b518c9b352fbee16e6d632adcb7a6d0760e2b7" - -meta if get_config? env = some "ci" then -require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "b941c425f6f0f1dc45fe13b850ffa7db1bb20d04" +require foundation from git "https://github.com/FormalizedFormalLogic/Foundation" @ "rename"