agda / agda

Agda is a dependently typed programming language / interactive theorem prover.
https://wiki.portal.chalmers.se/agda/pmwiki.php
Other
2.41k stars 339 forks source link

`agda-mode compile`: list of .el files might bitrot #7215

Closed andreasabel closed 2 months ago

andreasabel commented 2 months ago

Line elFiles <- filterM doesFileExist elFiles (last in following listing) considered harmful (error swallowing): https://github.com/agda/agda/blob/75d114fb04a9c0f3105427003c507da5500d6ef6/src/agda-mode/Main.hs#L233-L251 agda-mode contains a list of files that make up the emacs mode of Agda, so it is partially conscious. If one of these files is missing, there is a discrepancy between the mental model and reality, which should not be glossed over, but reported.