Stream: Coq users

Topic: Parsec not importing `guard`?

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.

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

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?

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.

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.

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.

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).

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.

Karl Palmskog (Jan 17 2022 at 16:24):

(but please create opam package too)

Yishuai Li (Feb 03 2022 at 22:06):

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

Last updated: Oct 13 2024 at 01:02 UTC