search

agda / agda

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

Add a beginner-friendly error / warning mode which points to the relevant docs #3230

Open gallais opened 6 years ago

gallais commented 6 years ago

I was reading an issue on the Idris bug tracker where people were puzzled by the use of "strictly positive". Given that we have great documentation covering these topics (case in point), I think it could be helpful to newcomers to point directly to them from inside our error messages.

This mode could be enabled via a flag e.g. verbose-errors.

nad commented 6 years ago

Such a mode should perhaps be enabled by default. Experienced users can turn it off if they want to. This can be somewhat awkward when switching between different versions of Agda in the Emacs mode, but I don't want to ask newcomers to customise Emacs before they begin using Agda.

One alternative is to require the use of a flag, but include this flag in the default value of agda2-program-args. Then it is easy to turn off verbose output, and by default the output on the command-line is not verbose. People who have already customised agda2-program-args might not discover this new flag, but perhaps that isn't so important.

andreasabel commented 2 years ago

For example (error message involving with) see