stdpp issueshttps://gitlab.mpi-sws.org/iris/stdpp/-/issues2024-03-18T16:05:30Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/issues/206Please create a tag for Coq 8.19 in Coq Platform 2024.012024-03-18T16:05:30ZRomain TetleyPlease create a tag for Coq 8.19 in Coq Platform 2024.01The Coq team released Coq `8.19.0` on January 24th, 2024.
The corresponding Coq Platform release `2024.01` should be released before **April 30th, 2024**.
It can be delayed in case of difficulties until May 15th, 2024, but this should be...The Coq team released Coq `8.19.0` on January 24th, 2024.
The corresponding Coq Platform release `2024.01` should be released before **April 30th, 2024**.
It can be delayed in case of difficulties until May 15th, 2024, but this should be an exception.
This issue is to inform you that to our (possibly a few days old) best knowledge the latest released version of your project (1.9.0) **does not work** with Coq `8.19.0`.
We tried to remove version restrictions in opam files and possibly make or configure files, but this did not suffice.
Please note that in Coq Platform CI (unlike Coq CI) we test only released / tagged versions. Coq CI appears to test this project, but has some special handling for your project which makes it difficult to retrieve the commit it tests for your project.
Could you please create a tag and opam package, or communicate us any existing tag that works with Coq branch v8.19, **preferably before March 31st, 2024**?
In case we might have to delay the Coq Platform release cause of issues with your project, we would prefer to be informed about the situation as early as possible.
In case the tag and opam package are available before March 31st, 2024, it will be included in an early Coq Platform beta release of the for Coq 8.19.0.
The working branch of Coq Platform, can be found here [main](https://github.com/coq/platform/tree/main).
It contains package pick [`~8.19~2024.01+beta1`](https://github.com/coq/platform/tree/main/package_picks/package-pick-8.19~2024.01+beta1.sh) which already supports Coq version `8.19.0` and contains already working (possibly patched / commit pinned) Coq Platform packages.
Please **don't** close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.
In any case, Coq Platform won't be released before this issue is closed!
Thanks!
P.S.: this issue has been created automatically based on CI status.
CC: https://github.com/coq/platform/issues/405https://gitlab.mpi-sws.org/iris/stdpp/-/issues/205Please tag a release with Coq 8.192024-03-18T16:56:10ZJulien PuydtPlease tag a release with Coq 8.19I saw you had commits for Coq 8.19 support, but didn't tag a release yet.
I'm working on updating the Coq ecosystem in Debian with Coq 8.19, so I'd like an official release.
There's no hurry: there's a handful of packages still blockin...I saw you had commits for Coq 8.19 support, but didn't tag a release yet.
I'm working on updating the Coq ecosystem in Debian with Coq 8.19, so I'd like an official release.
There's no hurry: there's a handful of packages still blocking anyway. This issue will help me track the progress.
Thanks,https://gitlab.mpi-sws.org/iris/stdpp/-/issues/204The bitvector library should ideally be accessible from the main coq-released...2024-03-11T21:10:46ZThibaut PéramiThe bitvector library should ideally be accessible from the main coq-released repositoryIdeally we would like the bitvector library in `stdpp-unstable` to be accessible from [Coq Released](https://github.com/coq/opam) repository. We need this because we'd like to put the Stdpp version of [`coq-sail`](https://github.com/rems...Ideally we would like the bitvector library in `stdpp-unstable` to be accessible from [Coq Released](https://github.com/coq/opam) repository. We need this because we'd like to put the Stdpp version of [`coq-sail`](https://github.com/rems-project/coq-sail) on it. Options includes:
- Putting `stdpp-unstable` on Coq Released
- Merging it in core Stdpp (Tracking issue #145 and #146)
- Creating a standalone `stdpp-bitvector` or `stdpp-bitvectors` or `stdpp-bv` and ship it to Coq Released separately.
What do you think of those options?https://gitlab.mpi-sws.org/iris/stdpp/-/issues/203simplify_map_eq sometimes fails to rewrite with `lookup_singleton_ne`2023-11-25T09:59:42ZRalf Jungjung@mpi-sws.orgsimplify_map_eq sometimes fails to rewrite with `lookup_singleton_ne`This came up in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/959, see the FIXMEs in gmap_view.v. This is probably related to old unification; `rewrite ->lookup_singleton_ne` fails but `rewrite lookup_singleton_ne` succeeds. So ...This came up in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/959, see the FIXMEs in gmap_view.v. This is probably related to old unification; `rewrite ->lookup_singleton_ne` fails but `rewrite lookup_singleton_ne` succeeds. So something similar to https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/497 could help.https://gitlab.mpi-sws.org/iris/stdpp/-/issues/202This is a test2023-11-20T13:53:40ZRalf Jungjung@mpi-sws.orgThis is a testjust ignore mejust ignore mehttps://gitlab.mpi-sws.org/iris/stdpp/-/issues/201stdpp constrains the template universe option.u02023-11-16T15:05:47ZKarl Palmskogstdpp constrains the template universe option.u0The file `fin_maps.v` is incompatible with any Coq code that uses `Some id`, due to universe constraints:
```coq
Definition x := Some id.
From stdpp Require Import fin_maps.
(*
Error: Universe inconsistency. Cannot enforce option.u0 <= b...The file `fin_maps.v` is incompatible with any Coq code that uses `Some id`, due to universe constraints:
```coq
Definition x := Some id.
From stdpp Require Import fin_maps.
(*
Error: Universe inconsistency. Cannot enforce option.u0 <= base.Equiv.u0 because base.Equiv.u0
<= Coq.Relations.Relation_Definitions.1 <= ID.u0 < option.u0.
*)
```
Another way to see the problem is the following:
```coq
From stdpp Require Import fin_maps.
Constraint ID.u0 <= option.u0.
(*
Error: Universe inconsistency. Cannot enforce ID.u0 <= option.u0 because option.u0 <= MapFold.u2
< Coq.Relations.Relation_Definitions.1 <= ID.u0.
*)
```
This was diagnosed on the [Coq Zulip](https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/stdpp.20universe.20inconistency.20with.20ID.20and.20fin_maps) with help from Gaëtan Gilbert.https://gitlab.mpi-sws.org/iris/stdpp/-/issues/200std++ collides with `Equations`: both define `simplify_eq`, and we mess up th...2023-11-01T14:33:35ZRalf Jungjung@mpi-sws.orgstd++ collides with `Equations`: both define `simplify_eq`, and we mess up their obligation tacticThe equations package seems to also contain a `simplify_eq` tactic
```
Ltac Equations.Init.simplify_eq
Ltac Coq.Init.Ltac.simplify_eq (shorter name to refer to it in current context is Ltac.simplify_eq)
```
stdpp's `simplify_eq` is a not...The equations package seems to also contain a `simplify_eq` tactic
```
Ltac Equations.Init.simplify_eq
Ltac Coq.Init.Ltac.simplify_eq (shorter name to refer to it in current context is Ltac.simplify_eq)
```
stdpp's `simplify_eq` is a notation, and the `Coq.Init` version seems to not be a problem, but when equations is imported, the tactic stops working. Instead one gets an obscure error, just saying "Not a negated primitive equality."
This is when equations is imported after std++. When I import equations first, it behaves in strange ways -- there's a different number of obligations generated and they also look different. I think equations might not like our `Global Obligation Tactic := idtac.`.https://gitlab.mpi-sws.org/iris/stdpp/-/issues/199Make `inv` and `oinv` work with numbers2023-10-30T20:51:23ZRalf Jungjung@mpi-sws.orgMake `inv` and `oinv` work with numbers`inversion 1` works but `inv 1` does not, which is a shame.
Thanks to Ike we now [know how to define a tactic that works on hypotheses as numbers](https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Writing.20a.20tactic.20th...`inversion 1` works but `inv 1` does not, which is a shame.
Thanks to Ike we now [know how to define a tactic that works on hypotheses as numbers](https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Writing.20a.20tactic.20that.20takes.20.22ident.20or.20term.20number.22.3F/near/396916621), but unfortunately defining `inv 1` s not trivial -- `inversion 1` will introduce the to-be-inverted term under some fresh name, which `inv` should clear, but I haven't found a way to tell `inversion` which name to use. @robbertkrebbers do you know if that is possible?
The alternative is to re-implement the logic that makes `inversion N` work, probably as something like "introduce N-1 terms, then introduce the next term under some chosen name, then revert all the other terms". But ideally we don't have to re-implement logic from core Coq tactics...https://gitlab.mpi-sws.org/iris/stdpp/-/issues/198Please create a tag for Coq 8.18 in Coq Platform 2023.102023-10-20T13:22:40ZMichael SoegtropPlease create a tag for Coq 8.18 in Coq Platform 2023.10The Coq team released Coq `8.18.0` on September 7th, 2023.
The corresponding Coq Platform release `2023.10` should be released before **November 30th, 2023**.
It can be delayed in case of difficulties until January 15th, 2023, but this s...The Coq team released Coq `8.18.0` on September 7th, 2023.
The corresponding Coq Platform release `2023.10` should be released before **November 30th, 2023**.
It can be delayed in case of difficulties until January 15th, 2023, but this should be an exception.
This issue is to inform you that to our (possibly a few days old) best knowledge the latest released version of your project (1.8.0) **does not work** with Coq `8.18.0`.
We tried to remove version restrictions in opam files and possibly make or configure files, but this did not suffice.
Please note that in Coq Platform CI (unlike Coq CI) we test only released / tagged versions. Coq CI appears to test this project, but has some special handling for your project which makes it difficult to retrieve the commit it tests for your project.
Could you please create a tag and opam package, or communicate us any existing tag that works with Coq branch v8.18, **preferably before October 31st, 2023**?
In case we might have to delay the Coq Platform release cause of issues with your project, we would prefer to be informed about the situation as early as possible.
In case the tag and opam package are available before October 31st, 2023, it will be included in an early Coq Platform beta release of the for Coq 8.18.0.
The working branch of Coq Platform, can be found here [main](https://github.com/coq/platform/tree/main).
It contains package pick [`~8.18+beta1`](https://github.com/coq/platform/tree/main/package_picks/package-pick-8.18+beta1.sh) which already supports Coq version `8.18.0` and contains already working (possibly patched / commit pinned) Coq Platform packages.
Please **don't** close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.
In any case, Coq Platform won't be released before this issue is closed!
Thanks!
P.S.: this issue has been created automatically based on CI status.
CC: https://github.com/coq/platform/issues/372https://gitlab.mpi-sws.org/iris/stdpp/-/issues/197`take_app_ge` has unneeded side-condition2023-10-05T14:10:29ZRobbert Krebbers`take_app_ge` has unneeded side-condition```coq
Lemma take_app_ge l k n :
length l ≤ n → take n (l ++ k) = l ++ take (n - length l) k.
```
`length l ≤ n` is not needed.
In fact, the stdlib has `firstn_app` which exactly the above std++ lemma without side-condition.```coq
Lemma take_app_ge l k n :
length l ≤ n → take n (l ++ k) = l ++ take (n - length l) k.
```
`length l ≤ n` is not needed.
In fact, the stdlib has `firstn_app` which exactly the above std++ lemma without side-condition.https://gitlab.mpi-sws.org/iris/stdpp/-/issues/196Ambiguous notations for vectors and telescopes2023-10-20T14:26:18ZRobbert KrebbersAmbiguous notations for vectors and telescopes```coq
From stdpp Require Import telescopes list.
Check [ tele ]. (* prints [tele] : list Type *)
Check [tele]. (* prints [tele] : tele *)
```
This is due to the notations in https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/stdpp/...```coq
From stdpp Require Import telescopes list.
Check [ tele ]. (* prints [tele] : list Type *)
Check [tele]. (* prints [tele] : tele *)
```
This is due to the notations in https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/stdpp/telescopes.v?ref_type=heads#L167
```
Notation "'[tele' ]" := (TeleO)
(format "[tele ]").
```
This shows that `[ tele ]` is parsed as a list, but it pretty prints without space, i.e., `[tele]`. When parsing this again, we end up with the empty telescopes.
See @snyke7's post below for a similar issue for vectors.https://gitlab.mpi-sws.org/iris/stdpp/-/issues/195multiset_simplify_singletons fails due to unification nonsense2023-08-28T14:37:01ZRalf Jungjung@mpi-sws.orgmultiset_simplify_singletons fails due to unification nonsenseI'd like to use `multiset_solver` [here](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris_heap_lang/lib/rw_spin_lock.v#L94) but it doesn't work. The problem turns out to be that `multiset_simplify_singletons` doesn't make progress...I'd like to use `multiset_solver` [here](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris_heap_lang/lib/rw_spin_lock.v#L94) but it doesn't work. The problem turns out to be that `multiset_simplify_singletons` doesn't make progress when it should. Specifically, `rewrite multiplicity_singleton` fails on `multiplicity x {[+ x +]} ≤ 0`. This is Coq's rewrite -- ssreflect rewrite works fine in the same situation.https://gitlab.mpi-sws.org/iris/stdpp/-/issues/194Refer to Iris documentation2023-08-03T17:15:57ZRobbert KrebbersRefer to Iris documentationThere is quite some documentation in Iris (setting up editor, how to use Propers, ...). We should include links to the relevant documentation in the std++ README.There is quite some documentation in Iris (setting up editor, how to use Propers, ...). We should include links to the relevant documentation in the std++ README.https://gitlab.mpi-sws.org/iris/stdpp/-/issues/193Rename Ltac iter into coq_list_iter2023-08-03T21:27:34ZRobbert KrebbersRename Ltac iter into coq_list_iterSee https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/931#note_94375
Bikeshed about gallina_list_iter, coq_list_iter, constr_list_iter, ...?See https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/931#note_94375
Bikeshed about gallina_list_iter, coq_list_iter, constr_list_iter, ...?https://gitlab.mpi-sws.org/iris/stdpp/-/issues/184Name mangling light causes noise in printing2023-07-17T15:38:42ZRobbert KrebbersName mangling light causes noise in printing```coq
From stdpp Require Import options.
Check forall x, x = 0.
(** Prints forall __x : nat, __x = 0 *)
```
This becomes worse when considering goals with quantifiers:
```coq
Lemma list_eq l1 l2 : (∀ i, l1 !! i = l2 !! i) → l1 = l2.
...```coq
From stdpp Require Import options.
Check forall x, x = 0.
(** Prints forall __x : nat, __x = 0 *)
```
This becomes worse when considering goals with quantifiers:
```coq
Lemma list_eq l1 l2 : (∀ i, l1 !! i = l2 !! i) → l1 = l2.
Proof.
revert l2.
(* Prints ∀ __l2 : list A, (∀ __i : nat, l1 !! __i = __l2 !! __i) → l1 = __l2 *)
```
This is totally unreadable.
Is there a way to fix this, or does this mean we should revert !475.https://gitlab.mpi-sws.org/iris/stdpp/-/issues/183New gmap representation causes set_solver / reflexivity to diverge2023-05-04T19:01:45ZMichael SammlerNew gmap representation causes set_solver / reflexivity to divergeWhen porting DimSum to https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/461, I noticed that some calls to `set_solver` diverge now whereas they used to succeed before. In particular, the following goal used by the solved by `set_so...When porting DimSum to https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/461, I noticed that some calls to `set_solver` diverge now whereas they used to succeed before. In particular, the following goal used by the solved by `set_solver` but it is not solved by it anymore as the new definition of gmap causes `reflexivity` to diverge:
```
Goal dom ((<["f":=1]> ∅) : gmap _ _) = dom ((<["f":=2]> ∅) : gmap _ _).
Proof.
Fail Timeout 2 set_solver.
Fail Timeout 2 reflexivity.
vm_compute. reflexivity.
Qed.
```https://gitlab.mpi-sws.org/iris/stdpp/-/issues/182`Countable` → `Finite` instance gives ambigous `encode`/`decode`.2023-05-03T08:38:53ZRobbert Krebbers`Countable` → `Finite` instance gives ambigous `encode`/`decode`.See discussion in https://mattermost.mpi-sws.org/iris/pl/teh4sqsgx7rjbjifkwjn8y5xee
@simongregersen if you have a self-contained example where it goes wrong, please post it here.See discussion in https://mattermost.mpi-sws.org/iris/pl/teh4sqsgx7rjbjifkwjn8y5xee
@simongregersen if you have a self-contained example where it goes wrong, please post it here.https://gitlab.mpi-sws.org/iris/stdpp/-/issues/181Associativity for scalar mulitiplication operator2023-04-28T17:37:42ZKimaya BedarkarAssociativity for scalar mulitiplication operatorThe notation "_ :* _" defined [here](https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/stdpp/base.v#L1089) is declared to be left associative. Does it make more sense for it to be right associative? (I am assuming this is the notation ...The notation "_ :* _" defined [here](https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/stdpp/base.v#L1089) is declared to be left associative. Does it make more sense for it to be right associative? (I am assuming this is the notation for scalar multiplication)
Additionally, to ensure compatibility with mathcomp in the future, could it be possible to add a check in the pipeline that tests if it is possible to import stdpp and ssreflect together?https://gitlab.mpi-sws.org/iris/stdpp/-/issues/180naive_solver does not solve trivial inconsistencies involving is_Some2023-04-12T14:25:20ZMarijn van Wezelmarijn.vanwezel@ru.nlnaive_solver does not solve trivial inconsistencies involving is_Some```
Example ex1 : is_Some (None : option nat) → False.
Proof.
Fail naive_solver. (* No matching clauses for match. *)
unfold is_Some. naive_solver. (* No more goals. *)
Qed.
Example ex2 : is_Some (Some 10).
Proof.
naive_solver. (*...```
Example ex1 : is_Some (None : option nat) → False.
Proof.
Fail naive_solver. (* No matching clauses for match. *)
unfold is_Some. naive_solver. (* No more goals. *)
Qed.
Example ex2 : is_Some (Some 10).
Proof.
naive_solver. (* No more goals. *)
Qed.
```https://gitlab.mpi-sws.org/iris/stdpp/-/issues/179set_solver does not unfold is_Some2023-04-12T14:25:48ZMarijn van Wezelmarijn.vanwezel@ru.nlset_solver does not unfold is_Some```coq
Example foo : is_Some (({[ 10 := 55 ]} : gmap nat nat) !! 10).
Proof.
Fail set_solver. (* No matching clauses for match. *)
unfold is_Some. set_solver. (* Works. *)
Qed.
``````coq
Example foo : is_Some (({[ 10 := 55 ]} : gmap nat nat) !! 10).
Proof.
Fail set_solver. (* No matching clauses for match. *)
unfold is_Some. set_solver. (* Works. *)
Qed.
```