Stream: Coq users

Topic: Parsec not importing `guard`?


view this post on Zulip Quinn (Jan 17 2022 at 15:59):

The following code appears in coq-parsec/test

From Parsec Require Import
     Core.
From Coq Require Import
     String.

(* From parsec/tests/Chunk.v *)
Definition parseLastChunk : parser unit :=
  many1 (expect "0"%char);;
  parseCRLF.

Definition parseChunk : parser string :=
  n <- guard (negb  Nat.eqb O) (N.to_nat <$> parseHex);;
  parseCRLF;;
  cs <- manyN n anyToken;;
  parseCRLF;;
  ret (string_of_list_ascii cs).

Locally, it compiles all the way until the definition of parseChunk, at which point it returns Error: The reference guard was not found in the current environment..

I believe the minimal replicator is

From Parsec Require Import Core.
Check guard.

I tried From Parsec Require Import Core Parser., which didn't help.

view this post on Zulip Karl Palmskog (Jan 17 2022 at 16:03):

I think you are going to need to ping the author of parsec for this @Yishuai Li

view this post on Zulip Yishuai Li (Jan 17 2022 at 16:14):

Hi,
I cannot reproduce the error on my side. Which version of Coq and Parsec are you using?

view this post on Zulip Yishuai Li (Jan 17 2022 at 16:15):

I see. guard was introduced after release v0.1.0. I'll release a new version now.

view this post on Zulip Quinn (Jan 17 2022 at 16:16):

what's in nixpkgs, and I don't have a particular commit of nixpkgs pinned so I think that means it's pulling in the latest one

Also, the latest commit to the coq-modules/parsec/default.nix file was september while the latest commit to the library was before that.

view this post on Zulip Yishuai Li (Jan 17 2022 at 16:23):

I believe Nix uses stable versions rather than branches, so I should first release a version, and then figure out how to inform Nix of the change.

view this post on Zulip Théo Zimmermann (Jan 17 2022 at 16:23):

Quinn said:

what's in nixpkgs, and I don't have a particular commit of nixpkgs pinned so I think that means it's pulling in the latest one

Also, the latest commit to the coq-modules/parsec/default.nix file was september while the latest commit to the library was before that.

It depends on how you've set things up, but more likely, if you haven't pinned nixpkgs for your specific Coq project, you are just using the version that is set in your system (and it likely doesn't auto-update without action from your part).

view this post on Zulip Théo Zimmermann (Jan 17 2022 at 16:24):

Yishuai Li said:

I believe Nix uses stable versions rather than branches, so I should first release a version, and then figure out how to inform Nix of the change.

That's correct. I can take care of doing the nixpkgs update if you want.

view this post on Zulip Karl Palmskog (Jan 17 2022 at 16:24):

(but please create opam package too)

view this post on Zulip Yishuai Li (Feb 03 2022 at 22:06):

https://github.com/coq/opam-coq-archive/pull/2092


Last updated: Feb 06 2023 at 11:03 UTC