From 441c94719ef1b4412ab080a206150a56db894152 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Wed, 21 Aug 2024 17:00:20 -0500
Subject: [PATCH] chore: add first commit

---
 .github/workflows/ci.yml                      | 38 +++++++++++++++++++
 Makefile                                      |  8 ++++
 P1/Makefile                                   |  7 ++++
 {lean => P1/lean}/.gitignore                  |  0
 lean/Shootout/Basic.lean => P1/lean/Main.lean |  0
 {lean => P1/lean}/lake-manifest.json          |  0
 {lean => P1/lean}/lakefile.lean               |  9 ++---
 {lean => P1/lean}/lean-toolchain              |  0
 README.md                                     |  4 ++
 lean/Main.lean                                |  3 --
 lean/Shootout.lean                            |  3 --
 11 files changed, 60 insertions(+), 12 deletions(-)
 create mode 100644 .github/workflows/ci.yml
 create mode 100644 Makefile
 create mode 100644 P1/Makefile
 rename {lean => P1/lean}/.gitignore (100%)
 rename lean/Shootout/Basic.lean => P1/lean/Main.lean (100%)
 rename {lean => P1/lean}/lake-manifest.json (100%)
 rename {lean => P1/lean}/lakefile.lean (67%)
 rename {lean => P1/lean}/lean-toolchain (100%)
 delete mode 100644 lean/Main.lean
 delete mode 100644 lean/Shootout.lean

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
new file mode 100644
index 0000000..0a04ba7
--- /dev/null
+++ b/.github/workflows/ci.yml
@@ -0,0 +1,38 @@
+name: Build
+on:
+  push:
+    branches:
+      - "main"
+  pull_request:
+  merge_group:
+
+permissions:
+  contents: write
+
+jobs:
+  build:
+    name: Build all tests
+    permissions:
+      pull-requests: write
+    runs-on: ubuntu-latest
+    steps:
+      - uses: DeterminateSystems/nix-installer-action@main
+
+      - name: Install cadical
+        run: nix profile install nixpkgs#cadical
+
+      - name: Checkout 🛎️
+        uses: actions/checkout@v3
+
+      - name: Install elan 🕑
+        run: |
+          set -o pipefail
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+          ~/.elan/bin/elan default stable
+          ~/.elan/bin/lean --version
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - name: Compile All Tests 🧐
+        run: |
+          make all
+
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..fd1b56e
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,8 @@
+.PHONY: all
+all: P1
+
+.PHONY: P1
+P1:
+	make -C P1/
+
+
diff --git a/P1/Makefile b/P1/Makefile
new file mode 100644
index 0000000..3e1ee6c
--- /dev/null
+++ b/P1/Makefile
@@ -0,0 +1,7 @@
+.PHONY: all
+all: lean
+
+.PHONY: lean
+lean:
+	@echo "Building Lean"
+	cd lean && lake build
diff --git a/lean/.gitignore b/P1/lean/.gitignore
similarity index 100%
rename from lean/.gitignore
rename to P1/lean/.gitignore
diff --git a/lean/Shootout/Basic.lean b/P1/lean/Main.lean
similarity index 100%
rename from lean/Shootout/Basic.lean
rename to P1/lean/Main.lean
diff --git a/lean/lake-manifest.json b/P1/lean/lake-manifest.json
similarity index 100%
rename from lean/lake-manifest.json
rename to P1/lean/lake-manifest.json
diff --git a/lean/lakefile.lean b/P1/lean/lakefile.lean
similarity index 67%
rename from lean/lakefile.lean
rename to P1/lean/lakefile.lean
index e85a1f2..7639ee2 100644
--- a/lean/lakefile.lean
+++ b/P1/lean/lakefile.lean
@@ -1,14 +1,11 @@
 import Lake
 open Lake DSL
 
-package «Shootout» where
+package «Main» where
   -- add package configuration options here
 
-lean_lib «Shootout» where
+@[default_target]
+lean_lib «Main» where
   -- add library configuration options here
 
 require LeanSAT from git "https://github.com/leanprover/leansat" @ "main"
-
-@[default_target]
-lean_exe «shootout» where
-  root := `Main
diff --git a/lean/lean-toolchain b/P1/lean/lean-toolchain
similarity index 100%
rename from lean/lean-toolchain
rename to P1/lean/lean-toolchain
diff --git a/README.md b/README.md
index 3a54208..fb27ef5 100644
--- a/README.md
+++ b/README.md
@@ -4,6 +4,10 @@ A theorem prover shootout, in the spirit of [The Great Computer Language Shootou
 for challenging verification problems that occur in practice.
 
 The current focus is on real-world (*not* synthetic) mixed bitvector and arithmetic problems.
+We **welcome pull requests** of new problems, and solutions to existing problems in different solvers.
 
 
+#### Directory Structure
 
+- Each problem is a toplevel directory, such as `P1/`.
+- Each solution for a given theorem prover is a subfolder, such as `P1/lean`.
diff --git a/lean/Main.lean b/lean/Main.lean
deleted file mode 100644
index b9b7eb3..0000000
--- a/lean/Main.lean
+++ /dev/null
@@ -1,3 +0,0 @@
-import «Shootout»
-
-def main : IO Unit := return ()
diff --git a/lean/Shootout.lean b/lean/Shootout.lean
deleted file mode 100644
index 0def1fa..0000000
--- a/lean/Shootout.lean
+++ /dev/null
@@ -1,3 +0,0 @@
--- This module serves as the root of the `Shootout` library.
--- Import modules here that should be built as part of the library.
-import «Shootout».Basic