fix buildscripts

Makefile

@@ -58,12 +58,11 @@ export BUILDDEP_OPAM_BODY
 
 # Create a virtual Opam package with the same deps as RefinedC, but no
 # build.
-builddep/refinedrust-builddep.opam: refinedrust.opam coq-lithium.opam Makefile
+builddep/refinedrust-builddep.opam: refinedrust.opam Makefile
 	@echo "# Creating builddep package."
 	@mkdir -p builddep
 	@echo "$$BUILDDEP_OPAM_BODY" > $@
-	@opam show -f depends: ./coq-lithium.opam >> $@
-	@opam show -f depends: ./refinedrust.opam | sed 's/"coq-lithium".*//g' >> $@
+	@opam show -f depends: ./refinedrust.opam >> $@
 	@echo "]" >> $@
 
 # Install the virtual Opam package to ensure that:

coq-lithium.opam

-opam-version: "2.0"
-name: "coq-lithium"
-synopsis: "Lithium proof automation for Iris"
-description: """
-Lithium proof automation for Iris
-"""
-license: "BSD-3-Clause"
-
-maintainer: ["Michael Sammler <msammler@mpi-sws.org>"
-             "Rodolphe Lepigre <lepigre@mpi-sws.org>"]
-authors: ["Michael Sammler" "Rodolphe Lepigre"]
-
-homepage: "https://plv.mpi-sws.org/refinedc"
-bug-reports: "https://gitlab.mpi-sws.org/iris/refinedc/issues"
-dev-repo: "git+https://gitlab.mpi-sws.org/iris/refinedc.git"
-
-depends: [
-  "coq" { (= "8.17.1" ) }
-  "coq-iris" { (= "dev.2023-09-11.0.1de1b311") | (= "dev") }
-  "coq-stdpp-unstable"
-  "dune" {>= "3.9.1"}
-  "coq-record-update" {= "0.3.0"}
-]
-
-build: [
-  ["dune" "subst"] {pinned}
-  ["dune" "build" "-p" name "-j" jobs]
-]

dune-project

 (lang dune 3.8)
 (name refinedrust)
 (package (name refinedrust))
-(package (name coq-lithium))
 (package (name coq-caesium-config-no-align) (allow_empty))
 (using coq 0.8)

refinedrust.opam

@@ -11,7 +11,11 @@ RefinedRust is a prototype framework for verifying safe and unsafe Rust code.
 license: "BSD-3-Clause"
 
 depends: [
-  "coq-lithium" {= version | = "dev"}
+  "coq" { (= "8.17.1" ) }
+  "coq-iris" { (= "dev.2023-09-11.0.1de1b311") | (= "dev") }
+  "coq-stdpp-unstable"
+  "dune" {>= "3.9.1"}
+  "coq-record-update" {= "0.3.0"}
   "coq-equations" { = "1.3+8.17" }
   "coq-lambda-rust" { = "dev" }
 ]

scripts/install-typesystem.sh

@@ -5,8 +5,5 @@
 # - REFINEDRUST_ROOT: the root directory of the RefinedRust checkout
 
 opam pin remove refinedrust -y
-opam pin remove coq-lithium -y
-opam remove coq-lithium -y
 opam remove refinedrust -y
-opam pin add coq-lithium.dev $REFINEDRUST_ROOT -y
 opam pin add refinedrust.dev $REFINEDRUST_ROOT -y

theories/lithium/benchmarks/dune

 (coq.theory
  (name lithium.benchmarks)
- (package coq-lithium)
+ (package refinedrust)
  (flags :standard -w -notation-overridden -w -redundant-canonical-projection)
  (synopsis "Lithium benchmarks")
  (theories lithium))