Huỳnh Trần Khanh (Jun 25 2021 at 03:10): Huỳnh Trần Khanh (Jun 25 2021 at 03:10):alright so i'm somewhat familiar with lean and i want to be able to read WasmCert source code. are there any resources to help me learn Isabelle? something interactive like the Natural Number Game would be great lol
Huỳnh Trần Khanh (Jun 25 2021 at 03:10):it seems that Isabelle is harder to learn than Lean right?
Huỳnh Trần Khanh (Jun 25 2021 at 03:10):thanks in advance btw
Huỳnh Trần Khanh (Jun 25 2021 at 03:41):and also it seems that the WasmCert specification introduces a lot of custom notation right
Huỳnh Trần Khanh (Jun 25 2021 at 03:42):like how can i read the custom notation, the notation is not defined anywhere in the code
Huỳnh Trần Khanh (Jun 25 2021 at 03:42):https://github.com/WasmCert/WasmCert-Isabelle
Kevin Kappelmann (Jun 25 2021 at 09:06):You can find a list of tutorials here: https://isabelle.in.tum.de/documentation.html
Manuel Eberl (Jun 25 2021 at 09:51):Please don't read the tutorial in the "Old Isabelle Manuals" section though.
I'd start with prog-prove.
Kevin Kappelmann (Jun 25 2021 at 09:52):Is there anything still useful in the old manual? If not, we should unlink it from the website
Manuel Eberl (Jun 25 2021 at 09:53):I don't really know.
Huỳnh Trần Khanh (Jun 25 2021 at 12:06):hmm alright how do i read the custom notation then?
Huỳnh Trần Khanh (Jun 25 2021 at 12:07):like there are a lot of symbols that i'm not familiar with
Huỳnh Trần Khanh (Jun 25 2021 at 12:07):they are not mentioned in any isabelle tutorial so i assume they must be custom
Lukas Stevens (Jun 25 2021 at 12:15):For normal notation, you can Ctrl+Click to go to the definition. For syntax translations, this doesn't work though.
Manuel Eberl (Jun 25 2021 at 12:18):What syntax are you talking about specifically?
Huỳnh Trần Khanh (Jun 25 2021 at 13:05):In the WasmCert formalization. The Ctrl+Click trick is really helpful, thank you!
Huỳnh Trần Khanh (Jun 25 2021 at 13:06):I don't plan to use Isabelle as my daily driver, it is so clumsy compared to Lean. (No I'm not starting another theorem prover war LOL) But I have to read the WasmCert formalization because I need to formalize WASM semantics in Lean and I'm looking for inspiration.
Huỳnh Trần Khanh (Jun 25 2021 at 13:08):Lukas Stevens said:
For normal notation, you can Ctrl+Click to go to the definition. For syntax translations, this doesn't work though.
Alright, so let's say I jumped to another file after hitting Ctrl+Click. How can I go back to the file I was opening?
Lukas Stevens (Jun 25 2021 at 13:12):There is the green back arrow in the top bar
Lukas Stevens (Jun 25 2021 at 13:13):on the far right
Lukas Stevens (Jun 25 2021 at 13:14):In Plugins > Global Options > jEdit > Shortcuts, the action is named Back and you can assign a shortcut for it (e.g. Alt+Left Arrow).
Mathias Fleury (Jun 25 2021 at 18:06):Kevin Kappelmann said:
Is there anything still useful in the old manual? If not, we should unlink it from the website
I find the chapter 5 useful (it is about dest/elim/... rules) and I don't know any alternative to it.
Last updated: Apr 25 2024 at 20:15 UTC