feat: initial commit

.github/workflows/ci.yml

@@ -0,0 +1,45 @@
+on:
+  push:
+  pull_request:
+
+name: Continuous Integration
+
+jobs:
+  build:
+    strategy:
+      matrix:
+        toolchain:
+          - "leanprover/lean4:4.5.0"
+          - "leanprover/lean4:4.6.0-rc1"
+    name: Build and test
+    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@v3
+
+      - name: List all files
+        run: |
+          find . -name "*.lean" -type f
+
+      - name: Select Lean version
+        run: |
+          echo "${{ matrix.toolchain }}" > lean-toolchain
+
+      - name: Lean version
+        run: |
+          lean --version
+
+      - name: Cache .lake
+        uses: actions/cache@v3
+        with:
+          path: .lake
+          key: ${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('lean-toolchain') }}
+
+      - name: Build the project
+        run: |
+          lake build

.gitignore

@@ -0,0 +1,3 @@
+/build
+/lakefile.olean
+/lake-packages/*

Main.lean

@@ -0,0 +1,4 @@
+import «Subverso»
+
+def main : IO Unit :=
+  IO.println s!"Hello, {hello}!"

README.md

@@ -0,0 +1,9 @@
+# Subverso - Verso's Library for Subprocesses
+
+Subverso is a support library that allows a
+[Verso](https://github.com/leanprover/verso) document to describe Lean
+code written in multiple versions of Lean. Verso itself may be tied to
+new Lean versions, because it makes use of new compiler features. This
+library will maintain broader compatibility with various Lean versions.
+
+

Subverso.lean

@@ -0,0 +1,3 @@
+-- This module serves as the root of the `Subverso` library.
+-- Import modules here that should be built as part of the library.
+import «Subverso».Basic

Subverso/Basic.lean

@@ -0,0 +1 @@
+def hello := "world"

lakefile.lean

@@ -0,0 +1,16 @@
+import Lake
+open Lake DSL
+
+package «subverso» where
+  -- add package configuration options here
+
+lean_lib «Subverso» where
+  -- add library configuration options here
+
+@[default_target]
+lean_exe «subverso» where
+  root := `Main
+  -- Enables the use of the Lean interpreter by the executable (e.g.,
+  -- `runFrontend`) at the expense of increased binary size on Linux.
+  -- Remove this line if you do not need such functionality.
+  supportInterpreter := true

lean-toolchain

@@ -0,0 +1 @@
+stable