Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

"Failed to desugar pulse extension text" with identifier errors #169

Closed
gebner opened this issue Aug 1, 2024 · 1 comment
Closed

"Failed to desugar pulse extension text" with identifier errors #169

gebner opened this issue Aug 1, 2024 · 1 comment

Comments

@gebner
Copy link
Contributor

gebner commented Aug 1, 2024

This is with the new #lang-pulse block from #168. If a Pulse definition has an identifier not found error, then we get an extra "Failed to desugar pulse extension text" error. Additionally, this error is shown not on the problematic identifier or its enclosing definition, but on a previous definition. There also seems to be an issue with incremental processing in the IDE; if you fix the error, check the file, and then introduce the error again, then there is no "Failed to desugar pulse extension text" message.

module BlockBug
#lang-pulse
open Pulse.Lib.Pervasives

// - Failed to desugar pulse extension text
let is_sublist (a b : Seq.seq nat) : prop = true

fn check_is_sublist (m: SiveT.t)
  requires emp
  ensures emp
{
  ()
}
@mtzguido
Copy link
Member

mtzguido commented Feb 7, 2025

Fixed by #306

@mtzguido mtzguido closed this as completed Feb 7, 2025
mtzguido added a commit to mtzguido/pulse that referenced this issue Feb 7, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants