Add changelog for 1.0.0 release (#288)

4ever2 · web-flow · commit 6464f7306e6c · 2026-03-09T01:17:46.000+01:00
diff --git a/.github/rocq-concert.opam.locked b/.github/rocq-concert.opam.locked
@@ -26,10 +26,7 @@ depends: [
   "coq-quickchick" {= "2.1.1"}
 ]
 build: [
-  [make "core"]
-  [make "html"] {with-doc}
-]
-install: [
-  [make "install"]
+  ["dune" "subst"] {dev}
+  ["dune" "build" "-p" name "-j" jobs "@install" "@runtest" {with-test} "@doc" {with-doc} "--stop-on-first-error"]
 ]
 dev-repo: "git+https://github.com/AU-COBRA/ConCert.git"
diff --git a/.gitignore b/.gitignore
@@ -88,6 +88,7 @@ nra.cache
 
 ## Dune
 _build/
+*.install
 
 ## Editors
 
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -6,3 +6,14 @@ 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]
+
+
+## [1.0.0] - 2026-03-09
+Initial release
+
+Compatible with Rocq 9.1
+
+
+
+[unreleased]: https://github.com/AU-COBRA/ConCert/compare/v1.0.0...HEAD
+[1.0.0]: https://github.com/AU-COBRA/ConCert/releases/tag/v1.0.0
diff --git a/examples/eip20/dune b/examples/eip20/dune
@@ -26,6 +26,7 @@
     ConCert.Execution
     ConCert.Execution.Test
     ConCert.Extraction
+    ConCert.Embedding
     ConCert.Embedding.Extraction
   )
 )
diff --git a/examples/escrow/dune b/examples/escrow/dune
@@ -26,6 +26,7 @@
     ConCert.Execution
     ConCert.Execution.Test
     ConCert.Extraction
+    ConCert.Embedding
     ConCert.Embedding.Extraction
   )
 )
diff --git a/examples/stackInterpreter/dune b/examples/stackInterpreter/dune
@@ -26,6 +26,7 @@
     ConCert.Execution
     ConCert.Execution.Test
     ConCert.Extraction
+    ConCert.Embedding
     ConCert.Embedding.Extraction
   )
 )
diff --git a/rocq-concert-examples.opam b/rocq-concert-examples.opam
@@ -14,13 +14,10 @@ bug-reports: "https://github.com/AU-COBRA/ConCert/issues"
 doc: "https://au-cobra.github.io/ConCert/toc.html"
 
 depends: [
-  "rocq-concert-examples" {= version}
+  "rocq-concert" {= version}
 ]
 
 build: [
-  [make "examples"]
-  [make "html"] {with-doc}
-]
-install: [
-  [make "install-examples"]
+  ["dune" "subst"] {dev}
+  ["dune" "build" "-p" name "-j" jobs "@install" "@runtest" {with-test} "@doc" {with-doc} "--stop-on-first-error"]
 ]
diff --git a/rocq-concert.opam b/rocq-concert.opam
@@ -31,9 +31,6 @@ depends: [
 ]
 
 build: [
-  [make "core"]
-  [make "html"] {with-doc}
-]
-install: [
-  [make "install"]
+  ["dune" "subst"] {dev}
+  ["dune" "build" "-p" name "-j" jobs "@install" "@runtest" {with-test} "@doc" {with-doc} "--stop-on-first-error"]
 ]

Original file line number	Diff line number	Diff line change
`@@ -26,10 +26,7 @@ depends: [`
`26`	`26`	`"coq-quickchick" {= "2.1.1"}`
`27`	`27`	`]`
`28`	`28`	`build: [`
`29`		`- [make "core"]`
`30`		`- [make "html"] {with-doc}`
`31`		`-]`
`32`		`-install: [`
`33`		`- [make "install"]`
	`29`	`+ ["dune" "subst"] {dev}`
	`30`	`+ ["dune" "build" "-p" name "-j" jobs "@install" "@runtest" {with-test} "@doc" {with-doc} "--stop-on-first-error"]`
`34`	`31`	`]`
`35`	`32`	`dev-repo: "git+https://github.com/AU-COBRA/ConCert.git"`
Original file line number	Diff line number	Diff line change
`@@ -26,6 +26,7 @@`
`26`	`26`	`ConCert.Execution`
`27`	`27`	`ConCert.Execution.Test`
`28`	`28`	`ConCert.Extraction`
	`29`	`+ ConCert.Embedding`
`29`	`30`	`ConCert.Embedding.Extraction`
`30`	`31`	`)`
`31`	`32`	`)`
Original file line number	Diff line number	Diff line change
`@@ -31,9 +31,6 @@ depends: [`
`31`	`31`	`]`
`32`	`32`
`33`	`33`	`build: [`
`34`		`- [make "core"]`
`35`		`- [make "html"] {with-doc}`
`36`		`-]`
`37`		`-install: [`
`38`		`- [make "install"]`
	`34`	`+ ["dune" "subst"] {dev}`
	`35`	`+ ["dune" "build" "-p" name "-j" jobs "@install" "@runtest" {with-test} "@doc" {with-doc} "--stop-on-first-error"]`
`39`	`36`	`]`