Timeline for What are the pros and cons of continuous checking over keychord-triggered checking?
Current License: CC BY-SA 4.0
13 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 6, 2022 at 20:43 | history | edited | taylor.2317 | CC BY-SA 4.0 |
added 2 characters in body
|
| Mar 2, 2022 at 11:51 | vote | accept | Trebor♦ | ||
| Feb 27, 2022 at 2:02 | comment | added | tydeu |
It is a bit inaccurate to describe what Lean is doing as just "checking". Technically, it is re-elaborating the file, a process which includes a bundle of other actions beyond syntax and type checking. For example, an #eval launchNukes statement will be re-evaluated each time the file is "checked" (launching nukes every time xD). I don't have much experience with other provers, so I am not sure if the checking in other prover is similarly more involved or if, on the other hand, they just do syntax/type checking.
|
|
| Feb 22, 2022 at 11:54 | answer | added | Jason Rute | timeline score: 4 | |
| Feb 20, 2022 at 9:22 | answer | added | Dima Pasechnik | timeline score: 7 | |
| Feb 19, 2022 at 19:52 | comment | added | Jason Rute | I feel like the question we are trying to get at is “why isn’t this feature in Agda (or Coq)”? Is it that it is hard to implement? Not important enough to implement? Or undesirable to users? | |
| Feb 19, 2022 at 17:12 | answer | added | Andrej Bauer | timeline score: 12 | |
| Feb 19, 2022 at 16:57 | comment | added | Kevin Buzzard | I don't really understand this question, as I mention in my answer. Doesn't continuous checking beat "check when I say so" hands down? | |
| Feb 19, 2022 at 15:28 | answer | added | Kevin Buzzard | timeline score: 4 | |
| Feb 19, 2022 at 15:21 | history | edited | Trebor♦ | CC BY-SA 4.0 |
deleted 5 characters in body; edited tags; edited title
|
| Feb 19, 2022 at 15:18 | comment | added | Trebor♦ | @JoshChen I was subconsciously thinking that only Lean has this as a default feature. AFAIK Isabelle also has this? | |
| Feb 19, 2022 at 15:09 | comment | added | Josh | I think this is a good question, but I think it could potentially be better if framed more broadly about the pros/cons of continuous vs on-demand checking, unless there's anything specific about Leans' implementation that you're interested in? | |
| Feb 19, 2022 at 15:05 | history | asked | Trebor♦ | CC BY-SA 4.0 |