Merge pull request #421 from hacspec/franziskus/v2-hax-cleanup

Remove some leftover hacspec-v2 strings

.github/workflows/test_installs.yml

@@ -13,7 +13,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
     - uses: actions/checkout@v3
-    - run: docker build -f .docker/Dockerfile . -t hacspec-v2
+    - run: docker build -f .docker/Dockerfile . -t hax
   setup_sh:
     if: ${{ github.event_name == 'workflow_dispatch'  || github.event_name == 'merge_group'   }}
     strategy:

cli/driver/src/exporter.rs

@@ -143,7 +143,7 @@ fn precompute_local_thir_bodies<'tcx>(
             })) {
                 Ok(x) => x,
                 Err(e) => {
-                    tcx.sess.span_err(span, format!("The THIR body of item {:?} was stolen.\nThis is not supposed to happen.\nThis is a bug in Hax's frontend.\nThis is discussed in issue https://github.com/hacspec/hacspec-v2/issues/27.\nPlease comment this issue if you see this error message!", ldid));
+                    tcx.sess.span_err(span, format!("The THIR body of item {:?} was stolen.\nThis is not supposed to happen.\nThis is a bug in Hax's frontend.\nThis is discussed in issue https://github.com/hacspec/hax/issues/27.\nPlease comment this issue if you see this error message!", ldid));
                     return (ldid, dummy_thir_body(tcx, span));
                 }
             };

engine/lib/import_thir.ml

@@ -1322,7 +1322,7 @@ and c_item_unwrapped ~ident (item : Thir.item) : item list =
                      (* TODO: introduce a Kind.TraitImplItem or
                         something. Otherwise we have to assume every
                         backend will see traits and impls as
-                        records. See https://github.com/hacspec/hacspec-v2/issues/271. *)
+                        records. See https://github.com/hacspec/hax/issues/271. *)
                      let ii_ident =
                        Concrete_ident.of_def_id Field item.owner_id
                      in

frontend/diagnostics/src/lib.rs

@@ -79,7 +79,7 @@ impl<S> std::fmt::Display for Diagnostics<S> {
                 f,
                 "something is not implemented yet.{}{}",
                 match issue_id {
-                    Some(id) => format!("This is discussed in issue https://github.com/hacspec/hacspec-v2/issues/{id}.\nPlease upvote or comment this issue if you see this error message."),
+                    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(),
                 },
                 match details {

frontend/exporter/src/types/copied.rs

@@ -429,7 +429,7 @@ pub enum UserType {
     //
     // In this case, we get a [rustc_middle::ty::ConstKind::Bound] in
     // [do_something], which we are not able to translate.
-    // See: https://github.com/hacspec/hacspec-v2/pull/209
+    // See: https://github.com/hacspec/hax/pull/209
 
     // Ty(Ty),
     // TypeOf(DefId, UserSubsts),

frontend/exporter/src/utils.rs

@@ -33,7 +33,7 @@ mod internal_helpers {
             builder.code(rustc_errors::DiagnosticId::Error(format!("HaxFront")));
             builder.note(
                 "⚠️ This is a bug in Hax's frontend.
-Please report this error to https://github.com/hacspec/hacspec-v2/issues with some context (e.g. the current crate)!",
+Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)!",
             );
             builder.emit()
         }};

hax-lib-macros/src/utils.rs

@@ -141,7 +141,7 @@ pub fn make_fn_decoration(
     let uid = ItemUid::fresh();
     let any_mut_ref = unmut_references_in_inputs(&mut signature);
     if any_mut_ref && matches!(kind, FnDecorationKind::Ensures { .. }) {
-        panic!("For now, ensures clause don't work on function that have `&mut` inputs (see https://github.com/hacspec/hacspec-v2/issues/290)")
+        panic!("For now, ensures clause don't work on function that have `&mut` inputs (see https://github.com/hacspec/hax/issues/290)")
     }
 
     let self_ident: Ident = syn::parse_quote! {self_};

setup.sh

@@ -54,7 +54,7 @@ install_rust_binaries() {
 
 # Provides the `hax-engine` binary
 install_ocaml_engine() {
-    # Fixes out of memory issues (https://github.com/hacspec/hacspec-v2/issues/197)
+    # Fixes out of memory issues (https://github.com/hacspec/hax/issues/197)
     {
         # Limit the number of thread spawned by opam
         export OPAMJOBS=$opam_jobs