Merge branch 'main' into paramDt

.github/workflows/main.yml

@@ -6,12 +6,15 @@ jobs:
   build:
     strategy:
       matrix:
-        name: [linux-x86_64, macOS-x86_64, macOS-arm64, windows-x86_64]
+        name: [linux-x86_64, linux-arm64, macOS-x86_64, macOS-arm64, windows-x86_64]
         build-type: [ release, debug ]
         include:
         - name: linux-x86_64
           os: ubuntu-20.04
           shell: bash
+        - name: linux-arm64
+          os: ubuntu-22.04-arm
+          shell: bash
         - name: macOS-x86_64
           os: macos-13
           shell: bash
@@ -29,6 +32,11 @@ jobs:
     # The type of runner that the job will run on
     runs-on: ${{ matrix.os }}
 
+    # cancel already running jobs for the same branch/pr/tag
+    concurrency:
+      group: build-${{ github.ref }}-${{ matrix.name }}:${{ matrix.build-type }}-${{ github.ref != 'refs/heads/main' || github.run_id }}
+      cancel-in-progress: ${{ github.repository != 'cvc5/ethos' || startsWith(github.ref, 'refs/pull/') }}
+
     steps:
     - name: Checkout code
       uses: actions/checkout@v4

NEWS.md

@@ -7,8 +7,10 @@ ethos 0.1.2 prerelease
 - The semantics for `eo::dt_constructors` is extended for instantiated parametric datatypes. For example calling `eo::dt_constructors` on `(List Int)` returns the list containing `cons` and `(as nil (List Int))`.
 - The semantics for `eo::dt_selectors` is extended for annotated constructors. For example calling `eo::dt_selectors` on `(as nil (List Int))` returns the empty list.
 
-ethos 0.1.1 prerelease
-======================
+ethos 0.1.1
+===========
+
+This release of Ethos is associated with the 1.2.1 release of the SMT solver cvc5.
 
 - When parsing Eunoia signatures, decimals and hexidecimals are never normalized, variables in binders are always unique for their name and type, and let is never treated as a builtin way of specifying macros. The options `--no-normalize-dec`, `--no-normalize-hex`, `--binder-fresh`, and `--no-parse-let` now only apply when parsing proofs and reference files.
 - Adds a new option `--normalize-num`, which also only applies when reference parsing. This option treats numerals as rationals, which can be used when parsing SMT-LIB inputs in logics where numerals are shorthand for rationals.

src/main.cpp

@@ -79,12 +79,14 @@ int main( int argc, char* argv[] )
       out << "           -t <tag>: enables the given trace tag (requires debug build)." << std::endl;
       out << "                 -v: verbose mode, enable all standard trace messages (requires debug build)." << std::endl;
       std::cout << out.str();
+      // exit immediately
+      exit(0);
       return 0;
     }
     else if (arg=="--show-config")
     {
       std::stringstream out;
-      out << "This is ethos version 0.1.0." << std::endl;
+      out << "This is ethos version 0.1.1." << std::endl;
       out << std::endl;
       size_t w = 15;
       out << std::setw(w) << "tracing : ";
@@ -95,6 +97,8 @@ int main( int argc, char* argv[] )
 #endif
       out << std::endl;
       std::cout << out.str();
+      // exit immediately
+      exit(0);
       return 0;
     }
     else if (arg=="-t")