lake + some packages

.github/workflows/lean_action_ci.yml

@@ -0,0 +1,14 @@
+name: Lean Action CI
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+      - uses: leanprover/lean-action@v1

.gitignore

@@ -0,0 +1 @@
+/.lake

Doug.lean

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

Doug/Basic.lean

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

Main.lean

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

README.md

@@ -0,0 +1 @@
+# doug

lake-manifest.json

@@ -0,0 +1,55 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/acmepjz/md4lean",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005",
+   "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": "6d2e06515f1ed1f74208d5a1da3a9cc26c60a7a0",
+   "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": "85e1e7143dd4cfa2b551826c27867bada60858e8",
+   "name": "BibtexQuery",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/mhuisi/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "bf066c328bcff19aa93adf4d24c4e896c0d4eaca",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "nightly",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/doc-gen4",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "5119580cd7510a440d54f67834c9024cc03a3e32",
+   "name": "«doc-gen4»",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.12.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "doug",
+ "lakeDir": ".lake"}

lakefile.lean

@@ -0,0 +1,22 @@
+import Lake
+open Lake DSL
+
+meta if get_config? env = some "dev" then -- dev is so not everyone has to build it
+require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "v4.12.0"
+
+package "doug" where
+  version := v!"0.1.0"
+
+lean_lib «Doug» where
+  -- add library configuration options here
+
+@[default_target]
+lean_exe "doug" where
+  root := `Main
+
+/--
+Doug
+-/
+script test (args) do
+  IO.println args
+  pure 0

lean-toolchain

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