Merge pull request #1296 from GaloisInc/at-release-2.12-prep

Prepare for 2.12 release by updating the change log, adding a Code of Conduct, and updating the pointer to recommended solver versions.

CHANGES.md

@@ -1,4 +1,4 @@
-# Next Release
+# 2.12.0
 
 ## Language changes
 * Updates to the layout rule.  We simplified the specification and made
@@ -15,6 +15,19 @@
   the stride for an enumeration, as opposed to the previous
   `[x, y .. z]` form (where the stride was computed from `x` and `y`).
 
+* Nested modules are now available (from pull request #1048). For example, the following is now valid Cryptol:
+
+        module SubmodTest where
+
+        import submodule B as C
+
+        submodule A where
+          propA = C::y > 5
+
+        submodule B where
+          y : Integer
+          y = 42
+
 ## New features
 
 * What4 prover backends now feature an improved multi-SAT procedure
@@ -30,6 +43,38 @@
   can be combined into a single line by separating them with `;`,
   which is necessary for stating a signature together with a
   definition, etc.
+  
+* There is a new `:set path` REPL option that provides an alternative to
+  `CRYPTOLPATH` for controlling where to search for imported modules
+  (issue #631).
+
+* The `cryptol-remote-api` server now natively supports HTTPS (issue
+  #1008), `newtype` values (issue #1033), and safety checking (issue
+  #1166).
+
+* Releases optionally include solvers (issue #1111). See the
+  `*-with-solvers*` files in the assets list for this release.
+
+## Bug fixes
+
+* Closed issues #422, #436, #619, #631, #633, #640, #680, #734, #735,
+  #759, #760, #764, #849, #996, #1000, #1008, #1019, #1032, #1033,
+  #1034, #1043, #1047, #1060, #1064, #1083, #1084, #1087, #1102, #1111,
+  #1113, #1117, #1125, #1133, #1142, #1144, #1145, #1146, #1157, #1160,
+  #1163, #1166, #1169, #1175, #1179, #1182, #1190, #1191, #1196, #1197,
+  #1204, #1209, #1210, #1213, #1216, #1223, #1226, #1238, #1239, #1240,
+  #1241, #1250, #1256, #1259, #1261, #1266, #1274, #1275, #1283, and
+  #1291.
+
+* Merged pull requests #1048, #1128, #1129, #1130, #1131, #1135, #1136,
+  #1137, #1139, #1148, #1149, #1150, #1152, #1154, #1156, #1158, #1159,
+  #1161, #1164, #1165, #1168, #1170, #1171, #1172, #1173, #1174, #1176,
+  #1181, #1183, #1186, #1188, #1192, #1193, #1194, #1195, #1199, #1200,
+  #1202, #1203, #1205, #1207, #1211, #1214, #1215, #1218, #1219, #1221,
+  #1224, #1225, #1227, #1228, #1230, #1231, #1232, #1234, #1242, #1243,
+  #1244, #1245, #1246, #1247, #1248, #1251, #1252, #1254, #1255, #1258,
+  #1263, #1265, #1268, #1269, #1270, #1271, #1272, #1273, #1276, #1281,
+  #1282, #1284, #1285, #1286, #1287, #1288, #1293, #1294, and #1295.
 
 # 2.11.0
 

CODE_OF_CONDUCT.md

@@ -0,0 +1,86 @@
+# Code of Conduct
+
+## Our Pledge
+
+We as members, contributors, and leaders pledge to make participation in our
+community a harassment-free experience for everyone, regardless of age, body
+size, visible or invisible disability, ethnicity, sex characteristics, gender
+identity and expression, level of experience, education, socio-economic status,
+nationality, personal appearance, race, caste, color, religion, or sexual identity
+and orientation.
+
+We pledge to act and interact in ways that contribute to an open, welcoming,
+diverse, inclusive, and healthy community.
+
+## Our Standards
+
+Examples of behavior that contributes to a positive environment for our
+community include:
+
+* Demonstrating empathy and kindness toward other people
+* Being respectful of differing opinions, viewpoints, and experiences
+* Giving and gracefully accepting constructive feedback
+* Accepting responsibility and apologizing to those affected by our mistakes,
+  and learning from the experience
+* Focusing on what is best not just for us as individuals, but for the
+  overall community
+
+Examples of unacceptable behavior include:
+
+* The use of sexualized language or imagery, and sexual attention or
+  advances of any kind
+* Trolling, insulting or derogatory comments, and personal or political attacks
+* Public or private harassment
+* Publishing others' private information, such as a physical or email
+  address, without their explicit permission
+* Other conduct which could reasonably be considered inappropriate in a
+  professional setting
+
+## Enforcement Responsibilities
+
+Project maintainers are responsible for clarifying and enforcing our standards of
+acceptable behavior and will take appropriate and fair corrective action in
+response to any behavior that they deem inappropriate, threatening, offensive,
+or harmful.
+
+Project maintainers have the right and responsibility to remove, edit, or reject
+comments, commits, code, wiki edits, issues, and other contributions that are
+not aligned to this Code of Conduct, and will communicate reasons for moderation
+decisions when appropriate.
+
+## Scope
+
+This Code of Conduct applies within all community spaces, and also applies when
+an individual is officially representing the community in public spaces.
+Examples of representing our community include using an official e-mail address,
+posting via an official social media account, or acting as an appointed
+representative at an online or offline event.
+
+## Enforcement
+
+Instances of abusive, harassing, or otherwise unacceptable behavior may
+be reported to the project maintainers responsible for enforcement at
+[cryptol@galois.com](mailto:cryptol@galois.com). All complaints will be
+reviewed and investigated promptly and fairly.
+
+All project maintainers are obligated to respect the privacy and security of the
+reporter of any incident.
+
+## Attribution
+
+This Code of Conduct is adapted from the [Contributor Covenant][homepage],
+version 2.1, available at
+[https://www.contributor-covenant.org/version/2/1/code_of_conduct.html][v2.1].
+
+Community Impact Guidelines were inspired by
+[Mozilla's code of conduct enforcement ladder][Mozilla CoC].
+
+For answers to common questions about this code of conduct, see the FAQ at
+[https://www.contributor-covenant.org/faq][FAQ]. Translations are available
+at [https://www.contributor-covenant.org/translations][translations].
+
+[homepage]: https://www.contributor-covenant.org
+[v2.1]: https://www.contributor-covenant.org/version/2/1/code_of_conduct.html
+[Mozilla CoC]: https://github.com/mozilla/diversity
+[FAQ]: https://www.contributor-covenant.org/faq
+[translations]: https://www.contributor-covenant.org/translations

README.md

@@ -46,9 +46,7 @@ Cryptol currently uses Microsoft Research's [Z3 SMT
 solver](https://github.com/Z3Prover/z3) by default to solve constraints
 during type checking, and as the default solver for the `:sat` and
 `:prove` commands.  Cryptol generally requires the most recent version
-of Z3, but you can see the specific version tested in CI by looking for
-the `Z3_VERSION` setting in [this
-file](https://github.com/GaloisInc/cryptol/blob/master/.github/workflows/ci.yml).
+of Z3, but you can see the specific version tested in CI by looking [here](https://github.com/GaloisInc/what4-solvers/releases/tag/snapshot-20210917).
 
 You can download Z3 binaries for a variety of platforms from their
 [releases page](https://github.com/Z3Prover/z3/releases). If you
@@ -77,7 +75,7 @@ Cryptol builds and runs on various flavors of Linux, Mac OS X, and
 Windows. We regularly build and test it in the following environments:
 
 - macOS 10.15, 64-bit
-- Ubuntu 18.04, 64-bit
+- Ubuntu 20.04, 64-bit
 - Windows Server 2019, 64-bit
 
 ## Prerequisites