coq-community / coq-ext-lib Goto Github PK

coq-ext-lib Bool has the same name as Coq bool, so installing it broke some of my other builds. For now I changed them to Require Import Bool.Bool

I am porting my code from Coq-8.4 to Coq-8.5pl1 and encountered the following problem:

Section WriterMonad.
  Variable s t : Type.
  Variable Monoid_s : Monoid s.

  Definition writer := writerT Monoid_s ident.
  Definition runWriter x := unIdent (@runWriterT s Monoid_s ident t x).
  Definition execWriter x:= snd (runWriter x).
  Definition evalWriter x:= fst (runWriter x).
End WriterMonad.

Definition Monoid_RthetaFlags : ExtLib.Structures.Monoid.Monoid RthetaFlags := ExtLib.Structures.Monoid.Build_Monoid RthetaFlagsAppend RthetaFlagsZero.

Definition flags_m : Type -> Type := writer Monoid_RthetaFlags.

Trying to compile the example above gives me the following error:

Error:
The term "Monoid_RthetaFlags" has type "Monoid.Monoid RthetaFlags"
while it is expected to have type "Monoid.Monoid ?s"
(universe inconsistency).
Makefile:274: recipe for target 'Rtheta.vo' failed

Any suggestions what might be causing this and what are possible workarounds? The code I have provided above is abridged, but if needed I can extract full self-containing example. Thanks!

In the MonadLaw, there is no right identity but based on my understanding, so far, we need to have left identity, right identity, and associativity. Is it a deliberate decision (or I am missing something)?

[1] Haskell Monad Law Page

The EqvWF_Build instance appears to lead astray typeclass resolution when performing unrelated rewrites.
Consider the following code snippet relying on itrees:

From ITree Require Import
     ITree Eq.Eq.

Goal forall {E R1 R2} (RR : R1 -> R2 -> Prop) (t1 t1': itree E R1) (t2 : itree E R2),
    eutt eq t1 t1' ->
    eutt RR t1 t2 ->
    False.
  intros * EQ1 EQ2.
  rewrite EQ1 in EQ2. (* Instantaneous *)
  Undo.

  Require Import ExtLib.Programming.Eqv.
  Fail Timeout 5 rewrite EQ1 in EQ2. (* Appears to loop, had it run a few minutes without success *)

  Remove Hints EqvWF_Build : typeclass_instances.

  rewrite EQ1 in EQ2. (* Instantaneous again *)
Abort.

Data.List fails to build with coq.dev (i.e., 8.10, if I understand correctly). It's probably a Coq bug, I just reported it here coq/coq#10870

Everything as up-to-date as possible (run with --verbose to show unavailable upgrades).
The following would require downgrades or uninstalls, but you may upgrade them explicitly:
  - coq-ext-lib.0.9.6

For coq-8.6 the library is at version 0.9.6, while for 8.7 it downgrades to 0.9.5.

One is in https://github.com/coq-community/coq-ext-lib/blob/master/theories/Data/Monads/ListMonad.v and one is in https://github.com/coq-community/coq-ext-lib/blob/master/theories/Data/List.v#L1-L123, and they're differently polymorphic.

(We noticed while wondering with @Janno whether ext-lib suffers from https://gitlab.mpi-sws.org/iris/stdpp/-/issues/80, and whether that causes MetaCoq/metacoq#580, but I'm not sure either way; at least ListMonad.v looks suspicious — and MetaCoq/metacoq#580 (comment) discusses the universe problem).

In theories/Structures/MonadLaws.v everything is commented out. In particular MonadLaws class which seems to be useful. Is that code which needs porting or it is being phased out?

The function digit2ascii from the Char module computes:

digit2ascii 10   ===> "B"

instead of "A".

current opam version fails to install with coq-8.6

I recently discovered this wonderful option: Set Typeclass Strict Resolution, which would help avoid infinite loop problems such as that motivating #106.

When looking for unifications of a goal with an instance of this class, we “freeze” all the existentials appearing in the goals, meaning that they are considered rigid during unification and cannot be instantiated.

You have to add more type annotations sometimes but as far as I can tell the types are ambiguous in such situations anyway. @gmalecha do you have any experience with that option?

The Coq team is planning to release Coq 8.13-beta1 on December 7, 2020
and Coq 8.13.0 on January 7, 2020.

Your project is currently scheduled for being bundled in the Windows installer.

We are currently testing commit 159c361
on branch https://github.com/coq-community/coq-ext-lib/tree/master
but we would like to ship a released version instead (a tag in git's slang).

Could you please tag that commit, or communicate us any other tag
that works with the Coq branch v8.13 at the latest 15 days before the
date of the final release?

Thanks!
CC: coq/coq#12334

See #24

There is notatoin conflict between extlib and standard library:

"` x : t <- c1 ;; c2" := bind c1 (fun x : t => c2) : monad_scope (default interpretation)
" `  t " := proj1_sig t : program_scope (default interpretation)

Version 0.9.4 installed via opam installs only .vo files, but not .v, like other opam library packages do.

It would be convenient to install sources as well as it would allow, for example, to quickly examine definitions pressing M-. in Emacs.

The Coq team released Coq 8.14+rc1 on September 17, 2021
and plans to release Coq 8.14.0 before October 31, 2021.
A corresponding Coq Platform releases should be released before November 30, 2021.
It can be dealyed in case of difficulties until January 31, 2022, but this should be an exception.

Coq CI is currently testing commit 968fb49
on branch https://github.com/coq-community/coq-ext-lib/tree/master
but we would like to ship a released version instead (a tag in git's slang).

Coq Platform is currently testing opam version dev
from official repository https://coq.inria.fr/opam/extra-dev.

Could you please create a tag, or communicate us any existing tag that works with
Coq branch v8.14, preferably 15 days before November 30, 2021
or earlier? 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.

Thanks!

P.S.: this issue has been creates semi-automatically.

CC: coq/platform#139

With recent patches to v8.4 branch we fixed build under MacOS. Now we need to update OPAM package in Coq OPAM repository. For this I need to have a new released version of ExtLib to build from.

Current OPAM package is referencing https://github.com/coq-ext-lib/coq-ext-lib/archive/v0.9.0.tar.gz
Perhaps you can release 0.9.1? I will be glad to submit an update to Coq OPAM package.

The Coq team released Coq 8.16+rc1 on June 01, 2022.
The corresponding Coq Platform release 2022.09 should be released before September 15, 2022.
It can be delayed in case of difficulties until October 15, 2022, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.16+rc1.

Coq Platform CI is currently testing opam package coq-ext-lib.0.11.6
from official repository https://coq.inria.fr/opam/released/packages/coq-ext-lib/coq-ext-lib.0.11.6/opam.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2022.09, please inform us as soon as possible and before August 31, 2022!

The working branch of Coq Platform, can be found here main.
It contains package pick ~8.16+rc1~2022.09~preview1 which already supports Coq version 8.16+rc1 and contains already working (possibly patched / commit pinned) Coq Platform packages.

In case you want to select a different version, 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: coq/platform#274

Original title: Use single-method class for Monad

Proposal: put bind and ret into their own classes, and let Monad be a dummy class indexed by those two:

Class Bind m := bind : forall a b, m a -> (a -> m b) -> m b.
Class Return m := ret : forall a, a -> m a.  (* And some are starting to prefer "pure" to "return" in Haskell *)
Class Monad m `{Bind m} `{Return m} := {}.
Instance MonadWith m `{Bind m} `{Return m} : Monad m := {| |}.

That way, bind and ret don't simplify away when used with concrete monads. This also allows ret to be shared with Applicative, since of course I am extending my proposal to all multi-field classes.

Is it possible to remove the requirement that the list has decidable equality from [to_nat_eq_member_eq]?

Show got complicated because it tried to do too much. It can generate string, list ascii, etc, any monoid with an injection from ASCII. This means that debugging instances is hard.

The Coq team released Coq 8.15.0 on January 13, 2022.
The corresponding Coq Platform release 2022.02 should be released before February 28, 2022.
It can be delayed in case of difficulties until April 11, 2022, but this should be an exception.

This issue is to inform you that the opam package we are currently testing in Coq Platform CI works fine with Coq 8.15.0.

Coq Platform CI is currently testing opam package coq-ext-lib.0.11.5
from official repository https://coq.inria.fr/opam/released/packages/coq-ext-lib/coq-ext-lib.0.11.5/opam.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.

In case you would prefer to see an updated or an older version in the upcoming Coq Platform 2022.02, please inform us as soon as possible and before February 14, 2022!

The working branch of Coq Platform, which already supports Coq version 8.15.0, can be found here https://github.com/coq/platform/tree/main.

In case you want to select a different version, 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: coq/platform#193

Monoids in coq-ext-lib are defined as follow:

Is there a special reason that the definition is a Record rather than a Class? I know that, under the hood, they are the same thing, but if my understanding is correct, you will not be able to declare a data structure as an instance of a Monoid unless you use Existing Class Monoid (why cannot be found in coq-ext-lib).

<$> is looser than >>=, causing f <$> g >>= h to be f <$> (g >>= h) rather than (f <$> g) >>= h, which is different from Haskell.
I'd propose:

• Align priority order with Haskell (wherever possible) to avoid such confusion.
• Document all notations somewhere.

We have Local Instance Applicative_Fun in ExtLib/Data/Fun.v. This makes it undiscoverable during typeclass search and I have to write:

liftA2 (AT:=(Applicative_Fun _)) f x y

instead of just:

liftA2 f x y

The issue is similar to https://gitlab.mpi-sws.org/iris/stdpp/-/issues/80 and mentioned in #121 and #123 (comment).

Is there some website that publicly hosts the coqdoc (html) for coq-ext-lib?

There should be universe polymorphic versions of, e.g. [list], [option], etc.

There should be a convention about this, e.g.

• Prefix with [p], e.g. plist, poption.
• Prefix with [_], e.g. _list, _option.

Everything else should be essentially the same.

Note there are still useful reasons to have monomorphic definitions, e.g. performance.

I am observing a strange error when using ExtLib. I am unsure if it is a bug or some sort of limitation, related to universes. In short, I've modified examples/StateGame.v ExtLib example, changing state type from Definition GameState: Type := (prod bool Z) with Record GameState : Type := mkGameState {on:bool; score:Z}.. This lead to the following error message:

Error:
Unable to satisfy the following constraints:

?State_m : "MonadState GameState (state GameState)"

At first glance MonadState_state instance should satisfy this constraint, but there is universe mismatch.
The full example is enclosed below:

Require Import Coq.ZArith.ZArith_base Coq.Strings.String.
Require Import ExtLib.Data.Monads.StateMonad ExtLib.Structures.Monads.

Section StateGame.
  
  Import MonadNotation.
  Local Open Scope Z_scope.
  Local Open Scope char_scope.
  Local Open Scope monad_scope.

  Definition GameValue : Type := Z.
  Record GameState : Type := mkGameState {on:bool; score:Z}.

  Variable m : Type -> Type.
  Context {Monad_m: Monad m}.
  Context {State_m: MonadState GameState m}.

  Fixpoint playGame (s: string) {struct s}: m GameValue :=
    match s with
    |  EmptyString =>
       v <- get ;; ret (score v)
    |  String x xs =>
       v <- get ;;
         match x, (on v) with
         | "a", true =>  put {| on := on v ; score := (score v) + 1 |}
         | "b", true => put {| on := on v ; score := (score v) - 1 |}
         | "c", _ =>   put {| on := negb (on v) ; score := score v |}
         |  _, _  =>   put v
         end ;; playGame xs
    end.

  Definition startState: GameState := {| on:=false; score:=0 |}.

End StateGame.

Definition main : GameValue :=
  (@evalState GameState GameValue (playGame (state GameState) "abcaaacbbcabbab") startState).

(* The following should return '2%Z' *)
Compute main.

Any reason that there is only transformer version WriterMonadT? Why there is no stand-alone version like you have for StateMonad?

I get:

coqc  -q  -R . ExtLib   Tactics/BoolTac
File "/srv/code/coq-ext-lib/theories/Tactics/BoolTac.v", line 18, characters 14-17:
Syntax error: [input_fun] or [ltac_def_kind] expected after [constr:global] (in [tacdef_body]).
make[2]: *** [Tactics/BoolTac.vo] Error 1
make[2]: Leaving directory `/srv/code/coq-ext-lib/theories'
make[1]: *** [coq] Error 2
make[1]: Leaving directory `/srv/code/coq-ext-lib/theories'
make: *** [theories] Error 2
ezyang@sabre:~/Dev/coq-ext-lib$ coqc --version
The Coq Proof Assistant, version 8.4pl2 (July 2013)
compiled on Jul 29 2013 08:19:10 with OCaml 3.12.1

It looks like run turned into a keyword.

Hi Gregory,

coq-ext-lib compilation is broken in the v8.5 branch by this patch:
coq/coq@b582db2

The error message I get is:

"coqc"  -q  -Q "theories" ExtLib   theories/Core/Type
File "./theories/Core/Type.v", line 27, characters 2-23:
Error: Cannot mix universe polymorphic and monomorphic declarations in sections.
Makefile.coq:358: recipe for target 'theories/Core/Type.vo' failed

a >=> (b >=> c) is the more efficient nesting when the composition unpacks-then-packs data (e.g., state, itrees).

Hi,

Thanks for ext-lib, it looks like a very carefully written library. I am considering dropping my home-made Monad typeclass for ExtLib, but I was wondering if you would be willing to add the let* x := p in q notation that matches whatOCaml has recently added.

It is possible to keep both, I think (_ <- _;; _ and let* _ := _ in _).

What do you think? I can propose a patch if you agree.

Thanks by advance!

 $ make                                                   
Makefile:3: coqdocjs/Makefile.doc: No such file or directory
make: *** No rule to make target 'coqdocjs/Makefile.doc'.  Stop.

Makefile.doc is indeed missing in the repository.

The package coq:ext-lib.1.0.0~beta2 does not compile anymore with Coq 8.5~beta3. See bench error. I updated the dependencies in ebb5b6b830a0addb21b9c2ad4f5afd98cf12d9e6.

Both Functor and Monad notations are declares at level 51, but Functor notation is left associative while Monad notation is right associative. I've solved this locally by changing the Functor notations to level 52, so if that's the right approach I'm happy to submit the tiny PR.

in String.v, the function ascii_cmp gives in correct results. For instance it says "a" > "b" but "b" < "c".

This appears to be because it is reading bits from the ASCII representation in the reverse order. The representation stores the least-significant bit first, but ascii_cmp treats the first bit as if it were the most-significant.

<$> and <*> are currently defined as right associative: https://github.com/coq-ext-lib/coq-ext-lib/blob/c0c934cd3c5fe24f55f41981e86a22a77f08f1ff/theories/Structures/Functor.v#L29 https://github.com/coq-ext-lib/coq-ext-lib/blob/c0c934cd3c5fe24f55f41981e86a22a77f08f1ff/theories/Structures/Applicative.v#L16 while they are left associative in Haskell: <$> <*>.
Is it designated on purpose, or is it worth changing them to left associative?

Say that I have:

Parameter parser : Type -> Type.
Instance Monad_parser : Monad parser. Admitted.
Parameter A B C D : Type.
Parameter pA : parser A.
Parameter pB : parser B.
Parameter pC : parser C.
Parameter f : A -> B -> C -> D.

To write a parser for D (without liftA2), I need:

Definition pD : parser D := ((f <$> pA) <*> pB) <*> pC.

where the parentheses are not required if the operators were left associative.

Most things in Structures should be universe polymorphic.

My original suggestion:

I have seen many projects putting together their own Monad stuff in Coq. Sometimes poorly. Ideally, they should all use ExtLib, but I think it has more than people really need and they are hesitant to bring another foundation library as a dependency.

Have you thought about breaking down ExtLib and moving Mondas into a separate small library? Call it something 'coq-monads' so people can easily find it. I think that will lower the barrier to entry and many more projects will adopt it. How knows, this could be a "gateway drug" to use the rest of ExtLib later :)

Comment from @gmalecha (PR #77):

I also wonder if there would be interest from the community to pull out Monad, Functor, Applicative as a separate library. There are a lot of libraries with exactly the same definitions and it is kind of annoying to have the same code in multiple dependencies because they don't interoperate. Specifically, I am thinking about stdpp, extlib, and meta-coq, but I wouldn't be surprised if there are others.

I am using this library and attempting to extract it to Haskell. In Haskell, there are default library and syntactical supports for monad, so it would be nice if the extracted code can use this facilities.

Currently, the resulting extracted code looks something like this:

data Monad m =
   Build_Monad (() -> Any -> m) (() -> () -> m -> (Any -> m) -> m)

ret :: (Monad a1) -> a2 -> a1
ret monad x =
  case monad of {
   Build_Monad ret0 _ -> unsafeCoerce ret0 __ x}

bind :: (Monad a1) -> a1 -> (a2 -> a1) -> a1
bind monad x x0 =
  case monad of {
   Build_Monad _ bind0 -> unsafeCoerce bind0 __ __ x x0}

data PMonad m =
   Build_PMonad (() -> Any -> Any -> m) (() -> () -> Any -> m -> (Any -> m)
                                        -> m)

type MonP m x = Any

pbind :: (PMonad a1) -> (MonP a1 a3) -> a1 -> (a2 -> a1) -> a1
pbind pMonad pu x x0 =
  case pMonad of {
   Build_PMonad _ pbind0 -> unsafeCoerce pbind0 __ __ pu x x0}

pMonad_Monad :: (Monad a1) -> PMonad a1
pMonad_Monad m =
  Build_PMonad (\_ -> unsafeCoerce (\_ x -> ret m x)) (\_ _ ->
    unsafeCoerce (\_ c f -> bind m c f))

I am wondering if some modules can be added as a default extraction configuration to collide monads on both sides?

It seems to me that fold on list is defined as folding from right to left, but fold on string is defined as folding from left to right. Is this intentional?

Because ext-lib defines modules like Bool, I've found that when you have ext-lib installed globally, it shadows too many of the standard modules for developments which just Require Bool. For example, Software Foundations cannot compile in the presence of coq-ext-lib. I've run into such discrepancies in other projects as well, where because of the presence of ext-lib (even though I never asked to use ext-lib), it was causing compilation behavior to differ between multiple environments. Finally I had to uninstall ext-lib just to keep a sane environment.

So my recommendation is to employ some mechanism to avoid shadowing anything that might be implicitly imported from the stdlib, like bools and tuples.

@gmalecha the goals of ext-lib and stdlibpp seem similar. I know you are using both.
Would it make sense to try to merge some common parts?
There also seems to be some overlap with math-classes.

When compiling ppsimpl (a new package for Coq's opam), I realized that it seems that coq_extlib conflicts with it because it shawos PositiveMap.t somehow. I feel that it is related to the "-R" problem discussed on Coq's mailing list, but I would be glad if you could just confirm this.