From a7b9963740aa849ad098c3428ddebf427cd92197 Mon Sep 17 00:00:00 2001
From: qwjyh <urataw421@gmail.com>
Date: Sun, 20 Oct 2024 16:17:37 +0900
Subject: [PATCH] lake + some packages

---
 .github/workflows/lean_action_ci.yml | 14 +++++++
 .gitignore                           |  1 +
 Doug.lean                            |  3 ++
 Doug/Basic.lean                      |  2 +
 Main.lean                            |  4 ++
 README.md                            |  1 +
 lake-manifest.json                   | 55 ++++++++++++++++++++++++++++
 lakefile.lean                        | 22 +++++++++++
 lean-toolchain                       |  1 +
 9 files changed, 103 insertions(+)
 create mode 100644 .github/workflows/lean_action_ci.yml
 create mode 100644 .gitignore
 create mode 100644 Doug.lean
 create mode 100644 Doug/Basic.lean
 create mode 100644 Main.lean
 create mode 100644 README.md
 create mode 100644 lake-manifest.json
 create mode 100644 lakefile.lean
 create mode 100644 lean-toolchain

diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml
new file mode 100644
index 0000000..09cd4ca
--- /dev/null
+++ b/.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
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..bfb30ec
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+/.lake
diff --git a/Doug.lean b/Doug.lean
new file mode 100644
index 0000000..d42e16a
--- /dev/null
+++ b/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
\ No newline at end of file
diff --git a/Doug/Basic.lean b/Doug/Basic.lean
new file mode 100644
index 0000000..38721e1
--- /dev/null
+++ b/Doug/Basic.lean
@@ -0,0 +1,2 @@
+def hello := "world"
+
diff --git a/Main.lean b/Main.lean
new file mode 100644
index 0000000..054c7b5
--- /dev/null
+++ b/Main.lean
@@ -0,0 +1,4 @@
+import Doug
+
+def main : IO Unit :=
+  IO.println s!"Hello, {hello}!"
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..86a62a5
--- /dev/null
+++ b/README.md
@@ -0,0 +1 @@
+# doug
\ No newline at end of file
diff --git a/lake-manifest.json b/lake-manifest.json
new file mode 100644
index 0000000..3530cbe
--- /dev/null
+++ b/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"}
diff --git a/lakefile.lean b/lakefile.lean
new file mode 100644
index 0000000..48fdeae
--- /dev/null
+++ b/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
diff --git a/lean-toolchain b/lean-toolchain
new file mode 100644
index 0000000..2bf5ad0
--- /dev/null
+++ b/lean-toolchain
@@ -0,0 +1 @@
+stable