From 0b06c2a0099be92128285ed8fa1d663cc41dee1b Mon Sep 17 00:00:00 2001
From: Calin Diacicov <diacicov.calin@gmail.com>
Date: Wed, 13 Nov 2024 19:21:39 +0100
Subject: [PATCH] Initial repository.

---
 .github/workflows/build.yml | 63 +++++++++++++++++++++++++++++++++++++
 code/dune                   |  6 ++++
 dune-project                |  3 ++
 3 files changed, 72 insertions(+)
 create mode 100644 .github/workflows/build.yml
 create mode 100644 code/dune
 create mode 100644 dune-project

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
new file mode 100644
index 0000000..44727c4
--- /dev/null
+++ b/.github/workflows/build.yml
@@ -0,0 +1,63 @@
+# This is a basic workflow to help you get started with Actions
+
+name: CI Computability
+
+# Controls when the action will run. 
+on:
+  # Triggers the workflow on push or pull request events but only for the master branch
+  push:
+    branches: [ master ]
+  pull_request:
+    branches: [ master ]
+  schedule:
+    # Run this workflow at 02:15 UTC every Tuesday to keep the cache from being
+    # evicted. A typical run with everything cached should take less than 10
+    # minutes.
+    - cron: 15 2 * * TUE
+
+  # Allows you to run this workflow manually from the Actions tab
+  workflow_dispatch:
+
+env:
+  # Set this to the version of Coq that should be used.
+  coq-version: 8.16.0
+  dune-version: 3.16.1
+  DUNE_CACHE_STORAGE_MODE: copy
+
+jobs:
+  build:
+    name: Build Computability
+    runs-on: ubuntu-22.04
+
+    steps:
+      # Checkout UniMath into the working directory
+      - name: Checkout UniMath.
+        uses: actions/checkout@v3
+        with:
+          repository: UniMath/UniMath
+          clean: false
+          path: .
+
+      # Checkout the current branch into SetHITs/
+      - name: Checkout Computability.
+        uses: actions/checkout@v3
+        with:
+          path: Computability
+
+      # Ideally we would use docker-coq. A setup currently takes about 7min
+      # before it starts compiling, with OCaml cached.
+      - name: Install OCaml.
+        uses: ocaml/setup-ocaml@v2
+        with:
+          ocaml-compiler: ocaml-variants.4.14.0+options,ocaml-option-flambda
+          dune-cache: true
+          opam-disable-sandboxing: true
+
+      - name: Install Dune
+        run: opam pin add dune ${{ env.dune-version }}
+      - name: Install Coq
+        run: opam pin add coq ${{ env.coq-version }}
+
+        # SetHITs is built using the flags specified in code/dune.
+      - name: Compile Computability.
+        run: opam exec -- dune build Computability --display=short --error-reporting=twice
\ No newline at end of file
diff --git a/code/dune b/code/dune
new file mode 100644
index 0000000..6cee613
--- /dev/null
+++ b/code/dune
@@ -0,0 +1,6 @@
+(include_subdirs qualified)
+
+(coq.theory
+ (name Computability)
+ (flags -w -notation-overridden -type-in-type)
+ (theories UniMath))
\ No newline at end of file
diff --git a/dune-project b/dune-project
new file mode 100644
index 0000000..f3b77aa
--- /dev/null
+++ b/dune-project
@@ -0,0 +1,3 @@
+(lang dune 3.16)
+(using coq 0.6)
+(name Computability)
\ No newline at end of file