Merge branch 'master' into use-kompilex

.github/ISSUE_TEMPLATE/bug-report.yaml

@@ -0,0 +1,92 @@
+---
+name: "[K-Bug] Report"
+description: Create a bug report to help us improve
+title: "[K-Bug] <TITLE>"
+labels: ["k-bug", "k"]
+
+body:
+  - type: markdown
+    attributes:
+      value: |
+        # Please Fill out the Form to the best of your ability.
+        ## Briefly what we're looking for:
+        ### Input Guidelines: 
+        1. *Minimized* files need to produce the bug.
+        2. When providing K definitions, a _single_ file should be provided (if possible), and as few modules and sentences as possible.
+        3. When providing programs or proofs, a _single_ program should be provided with a minimized definition which _quickly_ reproduces the issue.
+
+        ### Reproduction Steps
+        Steps to reproduce the behavior (including _code blocks_ with what to run, and _code blocks_ with resulting output).
+
+        ### Expected Behavior
+        A clear and concise description of what you expected to happen.
+        ---------------------------------------------------------------
+
+  - type: dropdown
+    attributes:
+      label: What component is the issue in?
+      options:
+        - Front-End 
+        - haskell-backend
+        - llvm-backend
+
+  - type: checkboxes
+    attributes:
+      label: Which command
+      description: You may select more than one
+      options:
+        - label: kompile
+        - label: kast
+        - label: krun
+        - label: kprove
+        - label: kprovex
+        - label: ksearch
+
+  - type: input
+    attributes:
+      label: What K Version?
+      placeholder: |
+        Run kompile --version and paste here
+    validations:
+      required: true
+
+  - type: dropdown
+    attributes:
+      label: "Operating System"
+      options:
+        - Linux
+        - MacOS (Intel)
+        - MacOS (Apple Silicon/AMD)
+    validations:
+      required: true
+
+  - type: textarea
+    attributes:
+      label: K Definitions (If Possible)
+      description: A _single_ program file with a minimized definition which _quickly_ reproduces the issue
+      placeholder: |
+        Files can be Drag & Dropped HERE 
+  - type: textarea
+    attributes:
+      label: Steps to Reproduce
+      description: Any information you think is relevant for us to understand the issue. Code blocks are acceptable.
+      placeholder: |
+        < ATTACH LOG HERE (IF POSSIBLE) > 
+    validations:
+      required: true
+  - type: textarea
+    attributes:
+      label: "Expected Results"
+      description: Please provide a brief description of what you expected to happen 
+      placeholder: < Drag & Drop files can be used to support expected result >
+    validations:
+      required: true
+
+
+  - type: markdown
+    attributes:
+      value: "## Thank you for contributing to our project!"
+  - type: markdown
+    attributes:
+      value: |
+        Thanks for taking the time to fill out this bug report.

.github/ISSUE_TEMPLATE/k-improvement-proposal.yaml

@@ -0,0 +1,98 @@
+---
+name: "[KIP] - K Improvement Proposal"
+description: Suggest a new feature for the K Language
+title: "[K-Improvement] <Title>"
+labels: ["request", "k", "improvement"]
+
+body:
+- type: markdown
+  attributes:
+    value: |
+      # First fill in the title (template provided).
+      ## Example:
+
+      [K-Improvement] - Use `foo` instead of `syntax` for declaring productions
+
+      # Motivation
+
+      -   Is there a semantics which you are developing which this feature would simplify?
+      -   Is this feature similar to a feature offered by another programming language?
+      -   Any other motivation?
+
+      # Example K Code
+
+      Provide a small, complete, and self-contained example of what you would like to be able to say in K.
+      Try to make it so that your example would `kompile` correctly if this feature were implemented.
+
+      ## Example:
+
+      I would like to be able to use `foo` instead of `syntax` for declaring AST nodes:
+
+      ```
+      module MYMODULE
+        imports BOOL
+
+        foo    Bar ::= "newBar" [function]
+        syntax Bar ::= "anotherBar"
+      endmodule
+      ```
+
+      # Documentation
+
+      Provide (initial) documentation for this new feature.
+
+      ## Example:
+
+      A user may choose to use `foo` instead of `syntax` when declaring new production in K.
+      The meaning is exactly identical to `syntax`, but it requires 3 fewer characters to type, which saves on average 17s/month of semantics development.
+
+      # Potential Alternatives/Workarounds
+      
+      If there is an obvious alternative way to implement this or an existing workaround, please briefly describe it here.
+
+      ## Example:
+
+      -   Users could also type `fo`, because it's even shorter. But because they are already pressing the `o` key, pressing `o` a second time has been shown to only increase the time per month by 2s (compared to the 17s overall), which means that the added benefit of programmers being familiar with the word `foo` outweighs the performance gains.
+      -   The keyword `bar` was also considered, but because `foo` has double-`o`, it's faster to type.
+
+      # Testing Approach
+      
+      If the feature is directly testable using the existing K test harness, provide an example test input/output here.
+      Otherwise, describe the testing approach you would use for this feature.
+
+      ## Example:
+
+      We could:
+
+      -   Modify `IMP` in the tutorial to use `foo` instead of `syntax` in a few places, or
+      -   Add the following definition to `tests/regression-new/foo-syntax.k`:
+
+          ```
+          module TEST
+            imports BOOL
+            configuration <k> $PGM:A </k>
+
+            syntax A ::= "blah"
+            foo A ::= "halb"
+
+            rule <k> blah => halb ... </k>
+          endmodule
+          ```
+
+          with the following input file:
+
+          ```
+          blah
+          ```
+
+          and expected output:
+
+          ```
+          halb
+          ```
+
+- type: textarea
+  attributes: 
+    label: Per the Examples above please provide some Improvement Suggestions
+    placeholder: <This field will be rendered into MarkDown> 
+    render: Markdown

.github/workflows/bump-version.yml

@@ -0,0 +1,33 @@
+name: 'Bump Version'
+on:
+  pull_request:
+    branches:
+      - 'master'
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  version-bump:
+    name: 'Version Bump'
+    runs-on: ubuntu-latest
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v3
+        with:
+          token: ${{ secrets.JENKINS_GITHUB_PAT }}
+          # fetch-depth 0 means deep clone the repo
+          fetch-depth: 0
+      - name: 'Update Version'
+        run: |
+          set -x
+          git config user.name devops
+          git config user.email devops@runtimeverification.com
+          if git diff --exit-code origin/${GITHUB_BASE_REF} origin/${GITHUB_HEAD_REF} -- package/version; then
+            ./package/version.sh bump $(git show origin/${GITHUB_BASE_REF}:package/version)
+          fi
+          ./package/version.sh sub
+          git add --update
+          if git commit --message "Set Version: $(cat package/version)"; then
+            git push origin HEAD:${GITHUB_HEAD_REF}
+          fi

.github/workflows/test-flake.yml

@@ -1,6 +1,10 @@
-name: "Test"
+name: 'Test Nix Flake'
 on:
   pull_request:
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
 jobs:
   compile-nix-flake:
     name: 'Nix flake'
@@ -30,4 +34,4 @@ jobs:
           signingKey: '${{ secrets.CACHIX_SIGNING_KEY }}'
 
       - name: 'Build K Framework'
-        run: GC_DONT_GC=1 nix build .
+        run: GC_DONT_GC=1 nix build .

.github/workflows/test.yml

@@ -1,6 +1,10 @@
 name: "Test"
 on:
   pull_request:
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
 jobs:
   test-nix:
     name: 'Nix'