This repository has been archived by the owner on Oct 25, 2023. It is now read-only.

`lake serve` fails when `lakefile.lean` doesn't compile #76

Closed

gebner opened this issue Jun 14, 2022 · 0 comments

Labels

bug

Milestone

Member

gebner commented Jun 14, 2022

Reopening #49 as this is a regression in Lake 3.1.1. lake serve now fails again when the lakefile has syntax errors.

The text was updated successfully, but these errors were encountered:

tydeu added the bug label

tydeu closed this as completed in

f26dbe1

tydeu added this to the v3.2.0 milestone

Kha pushed a commit to Kha/lake that referenced this issue


          fix: lake serve fallback regression

1a96b71

closes leanprover#76

Kha pushed a commit to Kha/lean4 that referenced this issue


          fix: lake serve fallback regression

854b154

closes leanprover/lake#76

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.