Timeline for What are the pros and cons of continuous checking over keychord-triggered checking?
Current License: CC BY-SA 4.0
12 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 22, 2022 at 21:01 | comment | added | Jason Rute | @Trebor Lean’s syntax is really customizable. While I don’t know Agda or have an example of what you mean, I doubt this is a significant difference between the two. | |
| Feb 20, 2022 at 8:43 | comment | added | Trebor♦ | In Agda for example, merely adding a symbol may cause a term to be parsed completely differently, because of the way Agda processes mixfixes. So the highlight will effectively be completely disabled. Lean doesn't seem to be affected by that. So does this mean Lean has a more restrictive syntax customization system? | |
| Feb 20, 2022 at 4:46 | comment | added | Mike Shulman | Coq and Agda will also immediately tell you when you've made a syntax error in the statement of a theorem. In Coq you write the statement and then evaluate it; the proof doesn't have to be present. In Agda you write the statement and define it to equal a hole. | |
| Feb 19, 2022 at 17:22 | comment | added | Kevin Buzzard | When writing e.g. the statement of a theorem I find it really helpful to be told immediately that I've made a syntax error. Now I have understood where the red lines occur and in particular if they're there because I'm in the middle of a sentence or if they're there because I goofed, I could not imagine going back to a non-continuous-checking system. As I say I still don't understand this question. It's like asking "I want to get from A to B as fast as possible. My two options are a fast car, and a slower car. What are the advantages of the slower car?" You're saying "it's only a bit slower". | |
| Feb 19, 2022 at 17:18 | comment | added | Andrej Bauer | @KevinBuzzard: You might be giving too much value to the continuous checking. It really isn't such a big deal to tell the proof assistant when to check things. Or is your experience with using Coq and Agda different? | |
| Feb 19, 2022 at 16:59 | comment | added | Kevin Buzzard | OK: edited. If you're still not happy then feel free to ask me to delete (perhaps explaining why) or feel free to edit yourself; I don't care about internet points, I am just trying to write a helpful answer to what I see as a rather weird question; if someone can point out some benefit to a non-continuous-checking system over what I am used to then this would change everything. | |
| Feb 19, 2022 at 16:59 | comment | added | Josh | I also agree with Andrej! I have zero skin in any supposed competition and mean no offense, but it does get tiresome to expect thoughtful comparisons for collective improvement of all our technologies and repeatedly encounter superlatives like "I can't imagine anything else" or "nothing could ever be better" | |
| Feb 19, 2022 at 16:56 | history | edited | Kevin Buzzard | CC BY-SA 4.0 |
rephrase to see if it makes Josh Chen happier; he had a valid criticism of the original version
|
| Feb 19, 2022 at 16:52 | comment | added | Kevin Buzzard | Point taken Josh: whilst I agree with Andrej, I will edit and I'll leave a comment under the question explaining why I think it's in some sense lousy. | |
| Feb 19, 2022 at 16:50 | comment | added | Andrej Bauer | It's not a competition between Lean and all the other proof assistants. | |
| Feb 19, 2022 at 16:12 | comment | added | Josh | With respect Kevin, this answer reads more like another ad for Lean (which has its place, just not here) instead of an attempt to seriously compare and explain the design decisions made in choosing continuous over non-continuous checking. | |
| Feb 19, 2022 at 15:28 | history | answered | Kevin Buzzard | CC BY-SA 4.0 |