From 92666ed16052aaa146d6d3811dd13871d69763cc Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Wed, 1 Nov 2023 05:32:07 -0400
Subject: [PATCH 1/8] upgrade to syn 2.x

---
 Cargo.lock                           | 8 ++++----
 Cargo.toml                           | 2 ++
 crates/formality-macros/Cargo.toml   | 6 ++++--
 crates/formality-macros/src/cast.rs  | 2 +-
 crates/formality-macros/src/debug.rs | 2 +-
 crates/formality-macros/src/parse.rs | 2 +-
 crates/formality-macros/src/term.rs  | 2 +-
 7 files changed, 14 insertions(+), 10 deletions(-)

diff --git a/Cargo.lock b/Cargo.lock
index 3651bb3b..6795f287 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -581,7 +581,7 @@ dependencies = [
  "expect-test",
  "proc-macro2",
  "quote",
- "syn 1.0.102",
+ "syn 2.0.27",
  "synstructure",
  "tracing",
 ]
@@ -1173,13 +1173,13 @@ dependencies = [
 
 [[package]]
 name = "synstructure"
-version = "0.12.6"
+version = "0.13.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f36bdaa60a83aca3921b5259d5400cbf5e90fc51931376a9bd4a0eb79aa7210f"
+checksum = "285ba80e733fac80aa4270fbcdf83772a79b80aa35c97075320abfee4a915b06"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 1.0.102",
+ "syn 2.0.27",
  "unicode-xid",
 ]
 
diff --git a/Cargo.toml b/Cargo.toml
index bb8a83db..520ac1c6 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -2,6 +2,8 @@
 name = "formality"
 version = "0.1.0"
 edition = "2021"
+license = "MIT OR APACHE-2"
+description = "Model of the Rust type system maintained by the Rust types team (in development)"
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
diff --git a/crates/formality-macros/Cargo.toml b/crates/formality-macros/Cargo.toml
index a75a6847..bdc73ee0 100644
--- a/crates/formality-macros/Cargo.toml
+++ b/crates/formality-macros/Cargo.toml
@@ -2,6 +2,8 @@
 name = "formality-macros"
 version = "0.1.0"
 edition = "2021"
+license = "MIT OR APACHE-2"
+description = "Macros used by a-mir-formality and formality-core"
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
@@ -11,8 +13,8 @@ proc-macro = true
 [dependencies]
 quote = "1.0.21"
 proc-macro2 = "1.0"
-syn = "1.0.102"
-synstructure = "0.12.6"
+syn = { version = "2.0", features = ["full"] }
+synstructure = "0.13.0"
 tracing = "0.1"
 convert_case = "0.6.0"
 
diff --git a/crates/formality-macros/src/cast.rs b/crates/formality-macros/src/cast.rs
index ef05b221..10efa4cb 100644
--- a/crates/formality-macros/src/cast.rs
+++ b/crates/formality-macros/src/cast.rs
@@ -91,5 +91,5 @@ fn downcast_to_variant(s: &synstructure::Structure, v: &VariantInfo) -> TokenStr
 }
 
 pub(crate) fn has_cast_attr(attrs: &[Attribute]) -> bool {
-    attrs.iter().any(|a| a.path.is_ident("cast"))
+    attrs.iter().any(|a| a.path().is_ident("cast"))
 }
diff --git a/crates/formality-macros/src/debug.rs b/crates/formality-macros/src/debug.rs
index e29fa0f0..2f7de119 100644
--- a/crates/formality-macros/src/debug.rs
+++ b/crates/formality-macros/src/debug.rs
@@ -237,7 +237,7 @@ fn debug_variant_with_attr(
 }
 
 fn get_grammar_attr(attrs: &[Attribute]) -> Option<syn::Result<FormalitySpec>> {
-    let attr = attrs.iter().find(|a| a.path.is_ident("grammar"))?;
+    let attr = attrs.iter().find(|a| a.path().is_ident("grammar"))?;
     Some(attr.parse_args())
 }
 
diff --git a/crates/formality-macros/src/parse.rs b/crates/formality-macros/src/parse.rs
index a3fa1f16..7e7f5b5e 100644
--- a/crates/formality-macros/src/parse.rs
+++ b/crates/formality-macros/src/parse.rs
@@ -206,7 +206,7 @@ fn lookahead(for_field: &Ident, op: Option<&FormalitySpecOp>) -> syn::Result<Lit
 }
 
 fn get_grammar_attr(attrs: &[Attribute]) -> Option<syn::Result<FormalitySpec>> {
-    let attr = attrs.iter().find(|a| a.path.is_ident("grammar"))?;
+    let attr = attrs.iter().find(|a| a.path().is_ident("grammar"))?;
     Some(attr.parse_args())
 }
 
diff --git a/crates/formality-macros/src/term.rs b/crates/formality-macros/src/term.rs
index a34609df..72c65847 100644
--- a/crates/formality-macros/src/term.rs
+++ b/crates/formality-macros/src/term.rs
@@ -40,7 +40,7 @@ fn remove_formality_attributes(input: &mut DeriveInput) {
         for variant in &mut v.variants {
             variant
                 .attrs
-                .retain(|attr| !attr.path.is_ident("grammar") && !attr.path.is_ident("cast"));
+                .retain(|attr| !attr.path().is_ident("grammar") && !attr.path().is_ident("cast"));
         }
     }
 }

From bedab834abb1a6ea3ee7c58fa49c7148cd73ecc5 Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Wed, 1 Nov 2023 05:10:46 -0400
Subject: [PATCH 2/8] rename to a-mir-formality

formality is taken on crates.io
---
 Cargo.lock                             | 36 +++++++++++++-------------
 Cargo.toml                             |  2 +-
 src/main.rs                            |  2 +-
 tests/associated_type_normalization.rs |  2 +-
 tests/coherence_overlap.rs             |  2 +-
 tests/projection.rs                    |  3 +--
 6 files changed, 23 insertions(+), 24 deletions(-)

diff --git a/Cargo.lock b/Cargo.lock
index 6795f287..1c8bd8bf 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -2,6 +2,24 @@
 # It is not intended for manual editing.
 version = 3
 
+[[package]]
+name = "a-mir-formality"
+version = "0.1.0"
+dependencies = [
+ "anyhow",
+ "clap 4.3.19",
+ "expect-test",
+ "formality-check",
+ "formality-core",
+ "formality-macros",
+ "formality-prove",
+ "formality-rust",
+ "formality-smir",
+ "formality-types",
+ "pretty_assertions",
+ "ui_test",
+]
+
 [[package]]
 name = "addr2line"
 version = "0.20.0"
@@ -522,24 +540,6 @@ dependencies = [
  "syn 1.0.102",
 ]
 
-[[package]]
-name = "formality"
-version = "0.1.0"
-dependencies = [
- "anyhow",
- "clap 4.3.19",
- "expect-test",
- "formality-check",
- "formality-core",
- "formality-macros",
- "formality-prove",
- "formality-rust",
- "formality-smir",
- "formality-types",
- "pretty_assertions",
- "ui_test",
-]
-
 [[package]]
 name = "formality-check"
 version = "0.1.0"
diff --git a/Cargo.toml b/Cargo.toml
index 520ac1c6..50e98397 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -1,5 +1,5 @@
 [package]
-name = "formality"
+name = "a-mir-formality"
 version = "0.1.0"
 edition = "2021"
 license = "MIT OR APACHE-2"
diff --git a/src/main.rs b/src/main.rs
index 6e883a15..d5d52038 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -1,3 +1,3 @@
 fn main() -> anyhow::Result<()> {
-    formality_core::with_tracing_logs(formality::main)
+    formality_core::with_tracing_logs(a_mir_formality::main)
 }
diff --git a/tests/associated_type_normalization.rs b/tests/associated_type_normalization.rs
index 9ce3abcd..06461886 100644
--- a/tests/associated_type_normalization.rs
+++ b/tests/associated_type_normalization.rs
@@ -1,4 +1,4 @@
-use formality::test_where_clause;
+use a_mir_formality::test_where_clause;
 
 const MIRROR: &str = "[
     crate core {
diff --git a/tests/coherence_overlap.rs b/tests/coherence_overlap.rs
index b30e9bbb..0efb4db8 100644
--- a/tests/coherence_overlap.rs
+++ b/tests/coherence_overlap.rs
@@ -1,6 +1,6 @@
 #![allow(non_snake_case)] // we embed type names into the names for our test functions
 
-use formality::test_program_ok;
+use a_mir_formality::test_program_ok;
 use formality_macros::test;
 
 #[test]
diff --git a/tests/projection.rs b/tests/projection.rs
index 4b13edcd..eaa68498 100644
--- a/tests/projection.rs
+++ b/tests/projection.rs
@@ -1,4 +1,4 @@
-use formality::test_where_clause;
+use a_mir_formality::test_where_clause;
 
 const NORMALIZE_BASIC: &str = "[
     crate test {
@@ -260,7 +260,6 @@ const PROJECTION_EQUALITY: &str = "[
     }
 ]";
 
-
 #[test]
 fn projection_equality() {
     expect_test::expect![[r#"

From d02a11ae63ebcb3453ab349cefde38b69eeb724e Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Wed, 1 Nov 2023 05:37:00 -0400
Subject: [PATCH 3/8] add a README and other metadata

---
 Cargo.toml                         | 3 +++
 crates/formality-macros/Cargo.toml | 2 ++
 crates/formality-macros/READE.md   | 5 +++++
 3 files changed, 10 insertions(+)
 create mode 100644 crates/formality-macros/READE.md

diff --git a/Cargo.toml b/Cargo.toml
index 50e98397..c5194b05 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -4,6 +4,9 @@ version = "0.1.0"
 edition = "2021"
 license = "MIT OR APACHE-2"
 description = "Model of the Rust type system maintained by the Rust types team (in development)"
+homepage = "https://rust-lang.github.io/a-mir-formality/"
+repository = "https://github.com/rust-lang/a-mir-formality/"
+readme = "README.md"
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
diff --git a/crates/formality-macros/Cargo.toml b/crates/formality-macros/Cargo.toml
index bdc73ee0..361a119b 100644
--- a/crates/formality-macros/Cargo.toml
+++ b/crates/formality-macros/Cargo.toml
@@ -4,6 +4,8 @@ version = "0.1.0"
 edition = "2021"
 license = "MIT OR APACHE-2"
 description = "Macros used by a-mir-formality and formality-core"
+homepage = "https://rust-lang.github.io/a-mir-formality/"
+repository = "https://github.com/rust-lang/a-mir-formality/"
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
diff --git a/crates/formality-macros/READE.md b/crates/formality-macros/READE.md
new file mode 100644
index 00000000..23e51871
--- /dev/null
+++ b/crates/formality-macros/READE.md
@@ -0,0 +1,5 @@
+# formality-macros
+
+Procedural macros used by the formality system.
+Don't import this crate directly.
+Check out formality-core instead.
\ No newline at end of file

From 3bd128f6dc7a17e7784e233122ee1449d44ef329 Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Wed, 1 Nov 2023 05:37:46 -0400
Subject: [PATCH 4/8] fix licensing

---
 Cargo.toml                         | 2 +-
 crates/formality-macros/Cargo.toml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cargo.toml b/Cargo.toml
index c5194b05..c58f3ec4 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -2,7 +2,7 @@
 name = "a-mir-formality"
 version = "0.1.0"
 edition = "2021"
-license = "MIT OR APACHE-2"
+license = "MIT OR Apache-2.0"
 description = "Model of the Rust type system maintained by the Rust types team (in development)"
 homepage = "https://rust-lang.github.io/a-mir-formality/"
 repository = "https://github.com/rust-lang/a-mir-formality/"
diff --git a/crates/formality-macros/Cargo.toml b/crates/formality-macros/Cargo.toml
index 361a119b..0d2346ae 100644
--- a/crates/formality-macros/Cargo.toml
+++ b/crates/formality-macros/Cargo.toml
@@ -2,7 +2,7 @@
 name = "formality-macros"
 version = "0.1.0"
 edition = "2021"
-license = "MIT OR APACHE-2"
+license = "MIT OR Apache-2.0"
 description = "Macros used by a-mir-formality and formality-core"
 homepage = "https://rust-lang.github.io/a-mir-formality/"
 repository = "https://github.com/rust-lang/a-mir-formality/"

From 69cbd88a3a3638e6a82fd6040303c7acaacadab7 Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Wed, 1 Nov 2023 05:42:01 -0400
Subject: [PATCH 5/8] make formality-core publishable

---
 crates/formality-core/Cargo.toml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/crates/formality-core/Cargo.toml b/crates/formality-core/Cargo.toml
index 3e589107..302b5b71 100644
--- a/crates/formality-core/Cargo.toml
+++ b/crates/formality-core/Cargo.toml
@@ -2,6 +2,10 @@
 name = "formality-core"
 version = "0.1.0"
 edition = "2021"
+license = "MIT OR Apache-2.0"
+description = "Language-independent formality system used by a-mir-formality"
+homepage = "https://rust-lang.github.io/a-mir-formality/"
+repository = "https://github.com/rust-lang/a-mir-formality/"
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
@@ -12,7 +16,7 @@ stacker = "0.1.15"
 tracing = "0.1"
 tracing-subscriber = {version = "0.3", default-features = false, features = ["env-filter", "fmt"]}
 tracing-tree = { version = "0.2" }
-formality-macros = { path = "../formality-macros" }
+formality-macros = { version = "0.1.0", path = "../formality-macros" }
 anyhow = "1.0.75"
 contracts = "0.6.3"
 

From e2a8af9660cb1e7d59dcf68ee803e23e82f111bd Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Wed, 1 Nov 2023 05:42:49 -0400
Subject: [PATCH 6/8] avoid "*" dependencies

---
 Cargo.lock                       | 6 +++---
 crates/formality-core/Cargo.toml | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/Cargo.lock b/Cargo.lock
index 1c8bd8bf..2941b86f 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -460,12 +460,12 @@ checksum = "34aa73646ffb006b8f5147f3dc182bd4bcb190227ce861fc4a4844bf8e3cb2c0"
 
 [[package]]
 name = "env_logger"
-version = "0.9.1"
+version = "0.10.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c90bf5f19754d10198ccb95b70664fc925bd1fc090a0fd9a6ebc54acc8cd6272"
+checksum = "85cdab6a89accf66733ad5a1693a4dcced6aeff64602b634530dd73c1f3ee9f0"
 dependencies = [
- "atty",
  "humantime",
+ "is-terminal",
  "log",
  "regex",
  "termcolor",
diff --git a/crates/formality-core/Cargo.toml b/crates/formality-core/Cargo.toml
index 302b5b71..c36cc26f 100644
--- a/crates/formality-core/Cargo.toml
+++ b/crates/formality-core/Cargo.toml
@@ -11,7 +11,7 @@ repository = "https://github.com/rust-lang/a-mir-formality/"
 
 [dependencies]
 lazy_static = "1.4.0"
-env_logger = "*"
+env_logger = "0.10.0"
 stacker = "0.1.15"
 tracing = "0.1"
 tracing-subscriber = {version = "0.3", default-features = false, features = ["env-filter", "fmt"]}

From 9320f16ae9fffb48c55ccd9980cbb6f85a36c5a6 Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Wed, 1 Nov 2023 05:44:35 -0400
Subject: [PATCH 7/8] add a README

---
 Cargo.lock                       | 2 +-
 crates/formality-core/Cargo.toml | 3 ++-
 crates/formality-core/README.md  | 4 ++++
 3 files changed, 7 insertions(+), 2 deletions(-)
 create mode 100644 crates/formality-core/README.md

diff --git a/Cargo.lock b/Cargo.lock
index 2941b86f..f218fa45 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -559,7 +559,7 @@ dependencies = [
 
 [[package]]
 name = "formality-core"
-version = "0.1.0"
+version = "0.1.1"
 dependencies = [
  "anyhow",
  "contracts",
diff --git a/crates/formality-core/Cargo.toml b/crates/formality-core/Cargo.toml
index c36cc26f..8908712c 100644
--- a/crates/formality-core/Cargo.toml
+++ b/crates/formality-core/Cargo.toml
@@ -1,11 +1,12 @@
 [package]
 name = "formality-core"
-version = "0.1.0"
+version = "0.1.1"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 description = "Language-independent formality system used by a-mir-formality"
 homepage = "https://rust-lang.github.io/a-mir-formality/"
 repository = "https://github.com/rust-lang/a-mir-formality/"
+readme = "README.md"
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
diff --git a/crates/formality-core/README.md b/crates/formality-core/README.md
new file mode 100644
index 00000000..35494e4d
--- /dev/null
+++ b/crates/formality-core/README.md
@@ -0,0 +1,4 @@
+# formality-core
+
+`formality_core` is the language independent part of a-mir-formality.
+It can be reused by other projects looking to model formal semantics of languages besides Rust.
\ No newline at end of file

From 0b3ef4b35cb1dfe8b9291a503d099fff7e71bd2e Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Thu, 2 Nov 2023 09:11:27 +0000
Subject: [PATCH 8/8] modify binary name in test runner

---
 tests/ui.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/ui.rs b/tests/ui.rs
index 9421ab68..05f758e4 100644
--- a/tests/ui.rs
+++ b/tests/ui.rs
@@ -6,7 +6,7 @@ fn main() -> Result<()> {
     let mut config = Config::rustc("tests/ui");
     // Prevent ui_test from trying to query `formality` for the host platform name
     config.host = Some("non of ya bizniz".into());
-    config.program.program = "target/debug/formality".into();
+    config.program.program = "target/debug/a-mir-formality".into();
     config.mode = Mode::Fail {
         require_patterns: false,
     };