search

impermeable / coq-waterproof

The Waterproof plugin for the Coq proof assistant allows you to write Coq proofs in a style that resembles handwritten mathematical proofs, designed to help university students with learning how to prove mathematical statements.
https://impermeable.github.io/
GNU Lesser General Public License v3.0
30 stars 9 forks source link

Feat test warnings and errors #80

Closed jim-portegies closed 3 weeks ago

jim-portegies commented 4 weeks ago

Add functionality to test messages and errors.

The core new functions are assert_fails_with_string and assert_feedback_with_strings.

Example usage:

assert_feedback_with_strings (fun () =>
  warn (Message.of_string "first warning");
  warn (Message.of_string "second warning"))
  Warning
["first warning"; "second warning"].
assert_fails_with_string
  (fun () => throw (Message.of_string "This error _should_ be raised."))
  "This error _should_ be raised.".

In addition

We also added more channels for feedback (inform, notice ...) and added a possibility for logging general feedback. We have removed all warnings during library compilation.