Merge pull request #1717 from cryspen/lean-proper-error-messages

[Lean] Proper error messages

Author: W95Psp

CHANGELOG.md

@@ -59,6 +59,7 @@ Changes to hax-lib:
 
 Changes to the Lean backend:
 - Improve support for functionalized loops (#1695)
+- Improve error messages, having each error (coming from the Lean backend) point to a specific github issue (#1717).
 
 Miscellaneous:
  - A lean tutorial has been added to the hax website (#1626)

hax-types/src/diagnostics/mod.rs

@@ -16,17 +16,13 @@ pub struct Diagnostics {
 impl std::fmt::Display for Diagnostics {
     fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
         match &self.kind {
-            Kind::Unimplemented { issue_id, details } => write!(
+            Kind::Unimplemented { issue_id:_, details } => write!(
                 f,
-                "something is not implemented yet.{}{}",
-                match issue_id {
-                    Some(id) => format!("This is discussed in issue https://github.com/hacspec/hax/issues/{id}.\nPlease upvote or comment this issue if you see this error message."),
-                    _ => "".to_string(),
-                },
+                "something is not implemented yet.{}",
                 match details {
                     Some(details) => format!("\n{}", details),
                     _ => "".to_string(),
-                }
+                },
             ),
             Kind::UnsupportedMacro { id } => write!(
                 f,