From 5e9be0ffe249e4ba8bcd1f38322a1aa3c16efad3 Mon Sep 17 00:00:00 2001
From: Maximus Gorog <mgorog@gmail.com>
Date: Mon, 27 Apr 2026 23:04:16 -0600
Subject: [PATCH] Add proprietary LICENSE; move CI to .forgejo/workflows/, run
 cubical-test
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- LICENSE: proprietary, all rights reserved.  Public availability of
  the repo grants no license; use requires written consent from
  mgorog@gmail.com.
- README: "Reusing this engine" → "Consuming the engine (with
  permission)" with explicit pointer to LICENSE.
- CI: workflow moved from .github/workflows/ to .forgejo/workflows/
  so forgejo's runner picks it up.  Workflow now also installs Rust,
  builds native/cubical/, and runs cubical-test (62/62 verification)
  rather than only running lake build (which would have failed at
  link time without libtopolei_cubical.a).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 .forgejo/workflows/lean_action_ci.yml | 24 ++++++++++++++++++++++++
 .github/workflows/lean_action_ci.yml  | 14 --------------
 LICENSE                               | 27 +++++++++++++++++++++++++++
 README.md                             |  7 ++++++-
 4 files changed, 57 insertions(+), 15 deletions(-)
 create mode 100644 .forgejo/workflows/lean_action_ci.yml
 delete mode 100644 .github/workflows/lean_action_ci.yml
 create mode 100644 LICENSE

diff --git a/.forgejo/workflows/lean_action_ci.yml b/.forgejo/workflows/lean_action_ci.yml
new file mode 100644
index 0000000..a494136
--- /dev/null
+++ b/.forgejo/workflows/lean_action_ci.yml
@@ -0,0 +1,24 @@
+name: Lean Action CI
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v5
+
+      - name: Install Rust toolchain
+        uses: dtolnay/rust-toolchain@stable
+
+      - name: Build Rust cubical kernel
+        run: cd native/cubical && cargo build --release
+
+      - uses: leanprover/lean-action@v1
+
+      - name: Run cubical-test
+        run: ./.lake/build/bin/cubical-test
diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml
deleted file mode 100644
index c48bd68..0000000
--- a/.github/workflows/lean_action_ci.yml
+++ /dev/null
@@ -1,14 +0,0 @@
-name: Lean Action CI
-
-on:
-  push:
-  pull_request:
-  workflow_dispatch:
-
-jobs:
-  build:
-    runs-on: ubuntu-latest
-
-    steps:
-      - uses: actions/checkout@v5
-      - uses: leanprover/lean-action@v1
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..b92876f
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,27 @@
+Copyright (c) 2026 Maximus Gorog. All rights reserved.
+
+This software and the associated source files, documentation, build
+scripts, configuration, and other materials in this repository
+(collectively, the "Software") are the proprietary and confidential
+property of the copyright holder.
+
+NO LICENSE IS GRANTED.  The presence of this Software in a publicly
+accessible repository does not, by itself, grant any permission to
+use, copy, modify, merge, publish, distribute, sublicense, link
+against, embed, or create derivative works of the Software, in whole
+or in part, for any purpose.
+
+Use of any kind — including but not limited to compilation, execution,
+incorporation into other software, or redistribution in any form —
+requires express prior written consent from the copyright holder.
+Unauthorized use is prohibited.
+
+For licensing inquiries, contact: mgorog@gmail.com
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE, AND
+NONINFRINGEMENT.  IN NO EVENT SHALL THE COPYRIGHT HOLDER BE LIABLE
+FOR ANY CLAIM, DAMAGES, OR OTHER LIABILITY, WHETHER IN AN ACTION OF
+CONTRACT, TORT, OR OTHERWISE, ARISING FROM, OUT OF, OR IN CONNECTION
+WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/README.md b/README.md
index 5b21ac8..d212bfb 100644
--- a/README.md
+++ b/README.md
@@ -21,7 +21,12 @@ preserves the Lean-level proofs.
 - `CubicalTest.lean`, `CubicalBench.lean` — engine smoke + property
   tests (62/62 passing) and microbenchmarks.
 
-## Reusing this engine
+## Consuming the engine (with permission)
+
+This Software is **proprietary**.  See `LICENSE` — no use is granted
+by virtue of the repository being public.  The instructions below
+are for the copyright holder and any party with prior written consent
+from `mgorog@gmail.com`.
 
 Add as a Lake dependency from another Lean 4 project: