chore: add first commit

.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
+

Makefile

@@ -0,0 +1,8 @@
+.PHONY: all
+all: P1
+
+.PHONY: P1
+P1:
+	make -C P1/
+
+

P1/Makefile

@@ -0,0 +1,7 @@
+.PHONY: all
+all: lean
+
+.PHONY: lean
+lean:
+	@echo "Building Lean"
+	cd lean && lake build

lean/lakefile.lean → 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

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`.