Skip to content

Commit

Permalink
refactor/ci: rename package name and fix (#5)
Browse files Browse the repository at this point in the history
  • Loading branch information
SnO2WMaN authored Oct 15, 2024
1 parent 1bfdc1b commit 1f22de2
Show file tree
Hide file tree
Showing 7 changed files with 17 additions and 142 deletions.
79 changes: 1 addition & 78 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
@@ -1,19 +1,12 @@
name: CI

# https://github.com/FormalizedFormalLogic/Foundation/blob/master/.github/workflows/ci.yml

on:
push:
branches:
- "master"
pull_request:
workflow_dispatch:

permissions:
contents: read
pages: write
id-token: write

concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: true
Expand All @@ -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
- uses: leanprover/lean-action@v1
2 changes: 1 addition & 1 deletion Arithmetization/Definability/Hierarchy.lean
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
import Arithmetization.Vorspiel.Lemmata
import Logic.FirstOrder.Arith.StrictHierarchy
import Foundation.FirstOrder.Arith.StrictHierarchy

/-!
Expand Down
2 changes: 1 addition & 1 deletion Arithmetization/ISigmaOne/Metamath/CodedTheory.lean
Original file line number Diff line number Diff line change
@@ -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

Expand Down
2 changes: 1 addition & 1 deletion Arithmetization/ISigmaOne/Metamath/Proof/Typed.lean
Original file line number Diff line number Diff line change
@@ -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

/-!
Expand Down
4 changes: 2 additions & 2 deletions Arithmetization/Vorspiel/Vorspiel.lean
Original file line number Diff line number Diff line change
@@ -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

Expand Down
56 changes: 8 additions & 48 deletions lake-manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand All @@ -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",
Expand All @@ -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",
Expand Down
14 changes: 3 additions & 11 deletions lakefile.lean
Original file line number Diff line number Diff line change
@@ -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"

0 comments on commit 1f22de2

Please sign in to comment.