From c5669e7858f3d308c583dd67bb2918966b0b504d Mon Sep 17 00:00:00 2001
From: 4ever2 <3417013+4ever2@users.noreply.github.com>
Date: Wed, 10 Jul 2024 22:45:04 +0200
Subject: [PATCH 1/4] Add changelog

---
 CHANGELOG.md | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 CHANGELOG.md

diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
index 0000000..2dd2344
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,16 @@
+# Changelog
+
+All notable changes to this project will be documented in this file.
+
+The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/),
+and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
+
+## [Unreleased]
+
+## [0.1.0] - 2024-07-10
+Initial release
+
+Compatible with Coq 8.17-8.19
+
+[unreleased]: https://github.com/AU-COBRA/coq-rust-extraction/compare/v0.1.0...HEAD
+[0.1.0]: https://github.com/AU-COBRA/coq-rust-extraction/releases/tag/v0.1.0

From f6cc4e7a9a51679f3bdb1b128c7576c808bf31de Mon Sep 17 00:00:00 2001
From: 4ever2 <3417013+4ever2@users.noreply.github.com>
Date: Wed, 10 Jul 2024 22:48:01 +0200
Subject: [PATCH 2/4] Add project info to README

---
 README.md | 25 +++++++++++++++++++++++--
 1 file changed, 23 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index 959b870..4dc94ef 100644
--- a/README.md
+++ b/README.md
@@ -1,3 +1,24 @@
-# rust-extraction
+# Coq Rust Extraction
+[![Build](https://github.com/AU-COBRA/coq-rust-extraction/actions/workflows/build.yml/badge.svg)](https://github.com/AU-COBRA/coq-rust-extraction/actions/workflows/build.yml)
+[![GitHub](https://img.shields.io/github/license/AU-COBRA/coq-rust-extraction)](https://github.com/AU-COBRA/coq-rust-extraction/blob/master/LICENSE)
+[![Documentation](https://img.shields.io/github/deployments/au-cobra/coq-rust-extraction/github-pages?label=docs)](https://au-cobra.github.io/coq-rust-extraction/)
 
-For documentation see [ConCert](https://github.com/AU-COBRA/ConCert)
+
+A framework for extracting Coq programs to Rust.
+
+## Meta
+
+- Author(s):
+  - Danil Annenkov (initial)
+  - Mikkel Milo (initial)
+  - Jakob Botsch Nielsen (initial)
+  - Bas Spitters (initial)
+  - Eske Hoy Nielsen
+- License: [MIT](LICENSE)
+- Compatible Coq versions: 8.17 or later
+- Additional dependencies: MetaCoq
+- Coq namespace: `RustExtraction`
+- Related publication(s):
+  - [Extracting functional programs from Coq, in Coq](https://arxiv.org/abs/2108.02995) doi:[10.1017/S0956796822000077](https://doi.org/10.1017/S0956796822000077)
+  - ["Extending MetaCoq Erasure: Extraction to Rust and Elm"](https://dannenkov.me/papers/extraction-rust-elm-coq-workshop2021.pdf)
+  - ["Extracting Smart Contracts Tested and Verified in Coq"](https://arxiv.org/abs/2012.09138) doi:[10.1145/3437992.3439934](https://doi.org/10.1145/3437992.3439934)

From ac86eac0e94100815da3a8a50a5397cb60b65e41 Mon Sep 17 00:00:00 2001
From: 4ever2 <3417013+4ever2@users.noreply.github.com>
Date: Wed, 10 Jul 2024 22:49:09 +0200
Subject: [PATCH 3/4] Add build instructions to README

---
 README.md | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/README.md b/README.md
index 4dc94ef..5f79bd7 100644
--- a/README.md
+++ b/README.md
@@ -22,3 +22,23 @@ A framework for extracting Coq programs to Rust.
   - [Extracting functional programs from Coq, in Coq](https://arxiv.org/abs/2108.02995) doi:[10.1017/S0956796822000077](https://doi.org/10.1017/S0956796822000077)
   - ["Extending MetaCoq Erasure: Extraction to Rust and Elm"](https://dannenkov.me/papers/extraction-rust-elm-coq-workshop2021.pdf)
   - ["Extracting Smart Contracts Tested and Verified in Coq"](https://arxiv.org/abs/2012.09138) doi:[10.1145/3437992.3439934](https://doi.org/10.1145/3437992.3439934)
+
+## Building and installation instructions
+
+The easiest way to install the latest released version is via [OPAM](https://opam.ocaml.org/doc/Install.html):
+
+```shell
+opam repo add coq-released https://coq.inria.fr/opam/released
+opam install coq-rust-extraction
+```
+
+To instead build and install manually, do:
+
+```shell
+opam repo add coq-released https://coq.inria.fr/opam/released
+git clone https://github.com/AU-COBRA/coq-rust-extraction.git
+cd coq-rust-extraction
+opam install . --deps-only
+make #or make -j <number-of-cores-on-your-machine> 
+make install
+```

From 03e75d8faef3bf6505a837cc93d08c8d1de2f1b1 Mon Sep 17 00:00:00 2001
From: 4ever2 <3417013+4ever2@users.noreply.github.com>
Date: Wed, 10 Jul 2024 22:50:19 +0200
Subject: [PATCH 4/4] Add documentation section in README

---
 README.md | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/README.md b/README.md
index 5f79bd7..dc78cfd 100644
--- a/README.md
+++ b/README.md
@@ -42,3 +42,9 @@ opam install . --deps-only
 make #or make -j <number-of-cores-on-your-machine> 
 make install
 ```
+
+## Documentation
+
+For documentation see [examples](/tests/theories/) and [generated CoqDoc](https://au-cobra.github.io/coq-rust-extraction/).
+
+Additional examples can be found in [ConCert](https://github.com/AU-COBRA/ConCert).