From 4598e77a9406d8040357c943a05dd1ab939932db Mon Sep 17 00:00:00 2001
From: Rutger Broekhoff
Date: Thu, 27 Jun 2024 01:56:05 +0200
Subject: Tidy up project

* Write README.md
* Add LICENSE
* Clean up some theorems and proofs
---
 README.md | 38 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 38 insertions(+)
 create mode 100644 README.md

(limited to 'README.md')

diff --git a/README.md b/README.md
new file mode 100644
index 0000000..125ea10
--- /dev/null
+++ b/README.md
@@ -0,0 +1,38 @@
+Coq Formalization for Mininix
+=============================
+
+[![License](https://img.shields.io/badge/License-BSD_3--Clause-blue.svg)](https://opensource.org/licenses/BSD-3-Clause)
+
+Mininix is a smaller version of the Nix expression language. This repository
+provides the mechanization of the semantics and reference interpreter for this
+language in the [Coq](https://coq.inria.fr/) proof assistant. For more details,
+I refer to my bachelor' thesis. I will link to it when it is made available on
+the [thesis archive](https://www.cs.ru.nl/bachelors-theses/) page of
+[iCIS](https://www.ru.nl/en/institute-for-computing-and-information-sciences).
+
+## Development
+
+During my thesis, I used Nix to manage the Coq installation for this thesis.
+If you use Nix, it should be easy to build/check the codebase. If not, this
+might be a bit more tricky.
+
+### Using Nix
+
+I have attached a `flake.nix` and `flake.lock` file, which should make my setup
+reproducible. Assuming a working Nix installation with flake support and the
+Nix command enabled, simply running `nix develop` followed by `make` should run
+`coqc` on all files. If you have a working [direnv](https://direnv.net/)
+installation, simply running `direnv allow` (after inspecting the `.envrc`
+file) should make the right version of Coq available.
+
+### Without Nix
+
+There are two things you need to have available. The current `flake.lock`
+ensures that we have the following software:
+
+- Coq, version 8.19.2.
+- [Coq-std++](https://gitlab.mpi-sws.org/iris/stdpp), version 1.10.0.
+  You may be able to install Coq-std++ via opam, as described in the README of
+  Coq-std++. However, your operating system's package repositories may also
+  provide a package. Consider taking a look at [the Repology
+  page](https://repology.org/project/coq-stdpp/packages).
-- 
cgit v1.2.3