From f200f93d2b9ba9c7a4b61da7f588f44e6476a3ec Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 11 Mar 2024 22:09:30 +0100
Subject: [PATCH] create new package for stdpp-bitvector library
---
_CoqProject | 7 +++---
coq-stdpp-bitvector.opam | 23 +++++++++++++++++++
.../bitblast.v | 0
.../bitvector.v | 0
.../bitvector_tactics.v | 4 ++--
stdpp_unstable/.keep | 0
tests/bitblast.v | 2 +-
tests/bitvector.v | 2 +-
tests/bitvector_tactics.v | 2 +-
9 files changed, 32 insertions(+), 8 deletions(-)
create mode 100644 coq-stdpp-bitvector.opam
rename {stdpp_unstable => stdpp_bitvector}/bitblast.v (100%)
rename {stdpp_unstable => stdpp_bitvector}/bitvector.v (100%)
rename {stdpp_unstable => stdpp_bitvector}/bitvector_tactics.v (99%)
create mode 100644 stdpp_unstable/.keep
diff --git a/_CoqProject b/_CoqProject
index 26c94883..80e5f22d 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -2,6 +2,7 @@
# `-Q $PACKAGE[/ ]` so that we can filter out the right ones for each package.
-Q stdpp stdpp
-Q stdpp_unstable stdpp.unstable
+-Q stdpp_bitvector stdpp.bv
# Fixing this one requires Coq 8.19
-arg -w -arg -argument-scope-delimiter
@@ -55,6 +56,6 @@ stdpp/telescopes.v
stdpp/binders.v
stdpp/ssreflect.v
-stdpp_unstable/bitblast.v
-stdpp_unstable/bitvector.v
-stdpp_unstable/bitvector_tactics.v
+stdpp_bitvector/bitblast.v
+stdpp_bitvector/bitvector.v
+stdpp_bitvector/bitvector_tactics.v
diff --git a/coq-stdpp-bitvector.opam b/coq-stdpp-bitvector.opam
new file mode 100644
index 00000000..6d8d5eb5
--- /dev/null
+++ b/coq-stdpp-bitvector.opam
@@ -0,0 +1,23 @@
+opam-version: "2.0"
+maintainer: "Ralf Jung <jung@mpi-sws.org>"
+authors: "The std++ team"
+license: "BSD-3-Clause"
+homepage: "https://gitlab.mpi-sws.org/iris/stdpp"
+bug-reports: "https://gitlab.mpi-sws.org/iris/stdpp/issues"
+dev-repo: "git+https://gitlab.mpi-sws.org/iris/stdpp.git"
+version: "dev"
+
+synopsis: "std++ bitvector"
+description: """
+Needs description
+"""
+tags: [
+ "logpath:stdpp.bv"
+]
+
+depends: [
+ "coq-stdpp" {= version}
+]
+
+build: ["./make-package" "stdpp_bitvector" "-j%{jobs}%"]
+install: ["./make-package" "stdpp_bitvector" "install"]
diff --git a/stdpp_unstable/bitblast.v b/stdpp_bitvector/bitblast.v
similarity index 100%
rename from stdpp_unstable/bitblast.v
rename to stdpp_bitvector/bitblast.v
diff --git a/stdpp_unstable/bitvector.v b/stdpp_bitvector/bitvector.v
similarity index 100%
rename from stdpp_unstable/bitvector.v
rename to stdpp_bitvector/bitvector.v
diff --git a/stdpp_unstable/bitvector_tactics.v b/stdpp_bitvector/bitvector_tactics.v
similarity index 99%
rename from stdpp_unstable/bitvector_tactics.v
rename to stdpp_bitvector/bitvector_tactics.v
index 02ab3586..65c8bcd5 100644
--- a/stdpp_unstable/bitvector_tactics.v
+++ b/stdpp_bitvector/bitvector_tactics.v
@@ -1,8 +1,8 @@
(** This file is still experimental. See its tracking issue
https://gitlab.mpi-sws.org/iris/stdpp/-/issues/146 for details on remaining
issues before stabilization. This file is maintained by Michael Sammler. *)
-From stdpp.unstable Require Export bitvector.
-From stdpp.unstable Require Import bitblast.
+From stdpp.bv Require Export bitvector.
+From stdpp.bv Require Import bitblast.
From stdpp Require Import options.
(** * bitvector tactics *)
diff --git a/stdpp_unstable/.keep b/stdpp_unstable/.keep
new file mode 100644
index 00000000..e69de29b
diff --git a/tests/bitblast.v b/tests/bitblast.v
index e68bbfc8..15bc7e09 100644
--- a/tests/bitblast.v
+++ b/tests/bitblast.v
@@ -1,4 +1,4 @@
-From stdpp.unstable Require Import bitblast.
+From stdpp.bv Require Import bitblast.
Local Open Scope Z_scope.
diff --git a/tests/bitvector.v b/tests/bitvector.v
index 13309159..5ea0529c 100644
--- a/tests/bitvector.v
+++ b/tests/bitvector.v
@@ -1,5 +1,5 @@
From stdpp Require Import strings.
-From stdpp.unstable Require Import bitvector.
+From stdpp.bv Require Import bitvector.
Check "notation_test".
Check (BV 10 3 = BV 10 5).
diff --git a/tests/bitvector_tactics.v b/tests/bitvector_tactics.v
index 46fda5c1..a2ed007e 100644
--- a/tests/bitvector_tactics.v
+++ b/tests/bitvector_tactics.v
@@ -1,5 +1,5 @@
From stdpp Require Import strings.
-From stdpp.unstable Require Import bitblast bitvector_tactics.
+From stdpp.bv Require Import bitblast bitvector_tactics.
Unset Mangle Names.
Local Open Scope Z_scope.
--
GitLab