search

coq / vscoq

Visual Studio Code extension for Coq
MIT License
335 stars 68 forks source link

Processing continues after a failed Require Import #917

Closed tchajed closed 1 week ago

tchajed commented 2 weeks ago

If you process any file with a Require Import that fails (eg, because the dependency isn't compiled), VsCoq proceeds over the Require Import and reports an error, but then continues going. This is very confusing because the rest of the file isn't going to work.

Software Foundations' Induction chapter (without running make) is a simple test case.

rtetley commented 1 week ago

I believe this is a duplicate of #877