From 9b35d687a52f53783e758ec60b9690bc0599dd0b Mon Sep 17 00:00:00 2001 From: Wolfgang Jeltsch Date: Mon, 21 Feb 2022 23:55:58 +0200 Subject: [PATCH 01/12] Switch automated builds from using `wget` to using `curl` --- .github/workflows/quick-and-dirty-build.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/quick-and-dirty-build.yaml b/.github/workflows/quick-and-dirty-build.yaml index 611020f..95e0583 100644 --- a/.github/workflows/quick-and-dirty-build.yaml +++ b/.github/workflows/quick-and-dirty-build.yaml @@ -22,7 +22,7 @@ jobs: - name: Get Isabelle from upstream if not found in cache run: | if [ ! -e /opt/Isabelle${{ env.isabelle-version }} ]; then - wget --no-verbose --output-document=- https://mirror.clarkson.edu/isabelle/dist/Isabelle${{ env.isabelle-version }}_linux.tar.gz | + curl --fail --silent --show-error https://mirror.clarkson.edu/isabelle/dist/Isabelle${{ env.isabelle-version }}_linux.tar.gz | tar --directory=/opt --extract --gzip fi - name: Install other Isabelle sessions From 1e328aca74b8633fb853685f7785fa22aa1b918f Mon Sep 17 00:00:00 2001 From: Wolfgang Jeltsch Date: Fri, 25 Feb 2022 21:54:50 +0200 Subject: [PATCH 02/12] Switch downloading of other repositories to using `curl` --- .github/workflows/quick-and-dirty-build.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/quick-and-dirty-build.yaml b/.github/workflows/quick-and-dirty-build.yaml index 95e0583..6ae6712 100644 --- a/.github/workflows/quick-and-dirty-build.yaml +++ b/.github/workflows/quick-and-dirty-build.yaml @@ -32,7 +32,7 @@ jobs: do account=`echo $repo | cut --delimiter=/ --fields=1` mkdir --parents /opt/other-isabelle-repos/$account - wget --no-verbose --output-document=/opt/other-isabelle-repos/$repo.zip https://github.com/$repo/archive/refs/heads/master.zip + curl --fail --silent --show-error https://github.com/$repo/archive/refs/heads/master.zip > /opt/other-isabelle-repos/$repo.zip unzip -d /opt/other-isabelle-repos/$account /opt/other-isabelle-repos/$repo.zip echo /opt/other-isabelle-repos/$repo-master/${{ env.source-path }} >> $HOME/.isabelle/Isabelle${{ env.isabelle-version }}/ROOTS done From fab5b5567f6e522e4f51b6b476291ec431182ce6 Mon Sep 17 00:00:00 2001 From: Wolfgang Jeltsch Date: Sat, 26 Feb 2022 03:54:05 +0200 Subject: [PATCH 03/12] Change repository URLs to the ultimate ones MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Apparently, `curl` doesn’t follow the redirection to the ultimate URLs under https://codeload.github.com/. Therefore, we now provide the destination URLs directly. --- .github/workflows/quick-and-dirty-build.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/quick-and-dirty-build.yaml b/.github/workflows/quick-and-dirty-build.yaml index 6ae6712..5c49d7e 100644 --- a/.github/workflows/quick-and-dirty-build.yaml +++ b/.github/workflows/quick-and-dirty-build.yaml @@ -32,7 +32,7 @@ jobs: do account=`echo $repo | cut --delimiter=/ --fields=1` mkdir --parents /opt/other-isabelle-repos/$account - curl --fail --silent --show-error https://github.com/$repo/archive/refs/heads/master.zip > /opt/other-isabelle-repos/$repo.zip + curl --fail --silent --show-error https://codeload.github.com/$repo/zip/refs/heads/master > /opt/other-isabelle-repos/$repo.zip unzip -d /opt/other-isabelle-repos/$account /opt/other-isabelle-repos/$repo.zip echo /opt/other-isabelle-repos/$repo-master/${{ env.source-path }} >> $HOME/.isabelle/Isabelle${{ env.isabelle-version }}/ROOTS done From e758bc66eeebe474532324d89c7af5256e25a15e Mon Sep 17 00:00:00 2001 From: Wolfgang Jeltsch Date: Mon, 7 Mar 2022 01:29:00 +0200 Subject: [PATCH 04/12] =?UTF-8?q?Replace=20=E2=80=9Csubject=20line?= =?UTF-8?q?=E2=80=9D=20by=20=E2=80=9Ctitle=E2=80=9D=20regarding=20pull=20r?= =?UTF-8?q?equests?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- CONTRIBUTING.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 06f80d2..27d2a03 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -30,7 +30,7 @@ When committing to this repository, please follow these rules: Merge `⟨other-branch⟩` into `⟨your-branch⟩` * When merging the branch of a pull request into the `master` branch, - put the subject line of the pull request into the body of the commit + put the title of the pull request into the body of the commit message and use a subject line of the following form: Merge `⟨branch⟩` of pull request #⟨pull-request-number⟩ into `master` From 8ab052831c7f90a329f182547e50fbcebf5f5f98 Mon Sep 17 00:00:00 2001 From: Wolfgang Jeltsch Date: Mon, 7 Mar 2022 02:33:00 +0200 Subject: [PATCH 05/12] Overhaul `quick-and-dirty-build.yaml` --- .github/workflows/quick-and-dirty-build.yaml | 31 ++++++++++++++------ 1 file changed, 22 insertions(+), 9 deletions(-) diff --git a/.github/workflows/quick-and-dirty-build.yaml b/.github/workflows/quick-and-dirty-build.yaml index 5c49d7e..0bac1ad 100644 --- a/.github/workflows/quick-and-dirty-build.yaml +++ b/.github/workflows/quick-and-dirty-build.yaml @@ -21,25 +21,38 @@ jobs: path: /opt/Isabelle${{ env.isabelle-version }} - name: Get Isabelle from upstream if not found in cache run: | - if [ ! -e /opt/Isabelle${{ env.isabelle-version }} ]; then - curl --fail --silent --show-error https://mirror.clarkson.edu/isabelle/dist/Isabelle${{ env.isabelle-version }}_linux.tar.gz | + if [ ! -e '/opt/Isabelle${{ env.isabelle-version }}' ] + then + curl --fail --silent --show-error \ + 'https://mirror.clarkson.edu/isabelle/dist/Isabelle${{ env.isabelle-version }}_linux.tar.gz' | tar --directory=/opt --extract --gzip fi - name: Install other Isabelle sessions run: | - mkdir --parent $HOME/.isabelle/Isabelle${{ env.isabelle-version }} + mkdir -p "$HOME/.isabelle/Isabelle${{ env.isabelle-version }}" for repo in ${{ env.other-isabelle-repos }} do - account=`echo $repo | cut --delimiter=/ --fields=1` - mkdir --parents /opt/other-isabelle-repos/$account - curl --fail --silent --show-error https://codeload.github.com/$repo/zip/refs/heads/master > /opt/other-isabelle-repos/$repo.zip - unzip -d /opt/other-isabelle-repos/$account /opt/other-isabelle-repos/$repo.zip - echo /opt/other-isabelle-repos/$repo-master/${{ env.source-path }} >> $HOME/.isabelle/Isabelle${{ env.isabelle-version }}/ROOTS + account=$(echo "$repo" | cut -d / -f 1) + mkdir -p "/opt/other-isabelle-repos/$account" + curl --fail --silent --show-error \ + "https://codeload.github.com/$repo/zip/refs/heads/master" \ + > "/opt/other-isabelle-repos/$repo.zip" + unzip -d "/opt/other-isabelle-repos/$account" \ + "/opt/other-isabelle-repos/$repo.zip" + echo \ + "/opt/other-isabelle-repos/$repo-master/${{ env.source-path }}" \ + >> "$HOME/.isabelle/Isabelle${{ env.isabelle-version }}/ROOTS" done - name: Check out repository uses: actions/checkout@v2 - name: Build - run: /opt/Isabelle${{ env.isabelle-version }}/bin/isabelle build -o quick_and_dirty -o document=pdf -P output -D ${{ env.source-path }} + run: | + '/opt/Isabelle${{ env.isabelle-version }}/bin/isabelle' \ + build \ + -o quick_and_dirty \ + -o document=pdf \ + -P output \ + -D '${{ env.source-path }}' - name: Upload document uses: actions/upload-artifact@v2 with: From b52c82ee5ca3a8d49ee0eb09fcab50d2f79838e5 Mon Sep 17 00:00:00 2001 From: Wolfgang Jeltsch Date: Thu, 10 Nov 2022 21:58:33 +0200 Subject: [PATCH 06/12] Switch to Isabelle2022 --- .github/workflows/quick-and-dirty-build.yaml | 2 +- README.md | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/quick-and-dirty-build.yaml b/.github/workflows/quick-and-dirty-build.yaml index 0bac1ad..0a428d9 100644 --- a/.github/workflows/quick-and-dirty-build.yaml +++ b/.github/workflows/quick-and-dirty-build.yaml @@ -2,7 +2,7 @@ name: Automated quick-and-dirty build env: source-path: src - isabelle-version: 2021-1 + isabelle-version: 2022 other-isabelle-repos: chapter-name: IOG session-name: Equivalence_Reasoner diff --git a/README.md b/README.md index 32ad961..21b967f 100644 --- a/README.md +++ b/README.md @@ -26,8 +26,8 @@ goals that involve `R` instead of `S`. Requirements ============ -You need Isabelle2021-1 to use this Isabelle library. You can obtain -Isabelle2021-1 from the [Isabelle website][isabelle]. +You need Isabelle2022 to use this Isabelle library. You can obtain +Isabelle2022 from the [Isabelle website][isabelle]. [isabelle]: https://isabelle.in.tum.de/ From 8f8bd656f12064f78d3b02fe7b7b60cea9ce60ec Mon Sep 17 00:00:00 2001 From: Wolfgang Jeltsch Date: Tue, 9 May 2023 01:12:49 +0300 Subject: [PATCH 07/12] Start using `jeltsch/actions-isabelle-build` --- .github/workflows/quick-and-dirty-build.yaml | 64 ++++---------------- 1 file changed, 11 insertions(+), 53 deletions(-) diff --git a/.github/workflows/quick-and-dirty-build.yaml b/.github/workflows/quick-and-dirty-build.yaml index 0a428d9..15888f1 100644 --- a/.github/workflows/quick-and-dirty-build.yaml +++ b/.github/workflows/quick-and-dirty-build.yaml @@ -1,60 +1,18 @@ -name: Automated quick-and-dirty build - -env: - source-path: src - isabelle-version: 2022 - other-isabelle-repos: - chapter-name: IOG - session-name: Equivalence_Reasoner - +name: 'Automated quick-and-dirty build' on: [push] - jobs: quick-and-dirty-build: runs-on: ubuntu-latest container: texlive/texlive:latest steps: - - name: Get Isabelle from cache if available - uses: actions/cache@v2 + - name: 'Check out repository' + uses: actions/checkout@v3 + - name: 'Build' + uses: jeltsch/actions-isabelle-build@master with: - key: isabelle-${{ env.isabelle-version }}-linux - path: /opt/Isabelle${{ env.isabelle-version }} - - name: Get Isabelle from upstream if not found in cache - run: | - if [ ! -e '/opt/Isabelle${{ env.isabelle-version }}' ] - then - curl --fail --silent --show-error \ - 'https://mirror.clarkson.edu/isabelle/dist/Isabelle${{ env.isabelle-version }}_linux.tar.gz' | - tar --directory=/opt --extract --gzip - fi - - name: Install other Isabelle sessions - run: | - mkdir -p "$HOME/.isabelle/Isabelle${{ env.isabelle-version }}" - for repo in ${{ env.other-isabelle-repos }} - do - account=$(echo "$repo" | cut -d / -f 1) - mkdir -p "/opt/other-isabelle-repos/$account" - curl --fail --silent --show-error \ - "https://codeload.github.com/$repo/zip/refs/heads/master" \ - > "/opt/other-isabelle-repos/$repo.zip" - unzip -d "/opt/other-isabelle-repos/$account" \ - "/opt/other-isabelle-repos/$repo.zip" - echo \ - "/opt/other-isabelle-repos/$repo-master/${{ env.source-path }}" \ - >> "$HOME/.isabelle/Isabelle${{ env.isabelle-version }}/ROOTS" - done - - name: Check out repository - uses: actions/checkout@v2 - - name: Build - run: | - '/opt/Isabelle${{ env.isabelle-version }}/bin/isabelle' \ - build \ - -o quick_and_dirty \ - -o document=pdf \ - -P output \ - -D '${{ env.source-path }}' - - name: Upload document - uses: actions/upload-artifact@v2 - with: - name: document - path: output/${{ env.chapter-name }}/${{ env.session-name }}/document.pdf + session-name: Equivalence_Reasoner + chapter-name: IOG + source-path: src + isabelle-version: 2022 + isabelle-mirror: https://mirror.clarkson.edu/isabelle/ + github-sessions: '' From 7358c742071ef66931545e63a60f6a3500c6df0e Mon Sep 17 00:00:00 2001 From: Wolfgang Jeltsch Date: Tue, 9 May 2023 01:29:07 +0300 Subject: [PATCH 08/12] Adapt to `jeltsch/actions-isabelle-build#6` --- .github/workflows/quick-and-dirty-build.yaml | 1 - 1 file changed, 1 deletion(-) diff --git a/.github/workflows/quick-and-dirty-build.yaml b/.github/workflows/quick-and-dirty-build.yaml index 15888f1..ff40129 100644 --- a/.github/workflows/quick-and-dirty-build.yaml +++ b/.github/workflows/quick-and-dirty-build.yaml @@ -14,5 +14,4 @@ jobs: chapter-name: IOG source-path: src isabelle-version: 2022 - isabelle-mirror: https://mirror.clarkson.edu/isabelle/ github-sessions: '' From af11198b0aa8ed68c5b45bfc4a688114bd58fb83 Mon Sep 17 00:00:00 2001 From: Wolfgang Jeltsch Date: Wed, 10 May 2023 20:50:09 +0300 Subject: [PATCH 09/12] Adapt workflow to `jeltsch/actions-isabelle-build#8` --- .github/workflows/quick-and-dirty-build.yaml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/quick-and-dirty-build.yaml b/.github/workflows/quick-and-dirty-build.yaml index ff40129..1dbf4f2 100644 --- a/.github/workflows/quick-and-dirty-build.yaml +++ b/.github/workflows/quick-and-dirty-build.yaml @@ -14,4 +14,5 @@ jobs: chapter-name: IOG source-path: src isabelle-version: 2022 + afp-sessions: '' github-sessions: '' From b6bb82b44f052beed9b5fd5cc514f6953fc67027 Mon Sep 17 00:00:00 2001 From: Wolfgang Jeltsch Date: Sun, 16 Jul 2023 19:59:32 +0300 Subject: [PATCH 10/12] Improve the layout of `imports` clauses --- src/Equivalence_Reasoner.thy | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Equivalence_Reasoner.thy b/src/Equivalence_Reasoner.thy index b8c0344..03d4306 100644 --- a/src/Equivalence_Reasoner.thy +++ b/src/Equivalence_Reasoner.thy @@ -133,10 +133,10 @@ section \Implementation\ text_raw \\label{implementation}\ theory Equivalence_Reasoner -imports - Main - "HOL-Eisbach.Eisbach_Tools" - \\Besides Eisbach, we use the @{attribute uncurry} attribute from the Eisbach tools.\ + imports + Main + "HOL-Eisbach.Eisbach_Tools" + \\Besides Eisbach, we use the @{attribute uncurry} attribute from the Eisbach tools.\ begin context begin From 1d01ec940d81b944c64c1b4889738a0248f6ea06 Mon Sep 17 00:00:00 2001 From: Wolfgang Jeltsch Date: Sun, 16 Jul 2023 22:58:59 +0300 Subject: [PATCH 11/12] Extend and improve the contribution rules --- CONTRIBUTING.md | 21 ++++++++++++++++----- 1 file changed, 16 insertions(+), 5 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 27d2a03..ddc2517 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -1,7 +1,17 @@ -Commit rules -============ +Rules for branches +================== -When committing to this repository, please follow these rules: + * Use a branch name of the form `⟨type⟩/⟨topic⟩`. Here, `⟨type⟩` + refers to the type of contribution as given by the label of the form + `type: ⟨type⟩` of the pull request associated with the branch. + + * For the `⟨topic⟩` part of the branch name, use only lowercase Latin + letters, Arabic numerals, and ASCII dashes, with the latter also + serving as separators of words. + + +Rules for commits[^original-commit-rules] +========================================= * Put only related changes into a single commit. @@ -38,5 +48,6 @@ When committing to this repository, please follow these rules: Here, `⟨branch⟩` refers to the name of the branch without the GitHub account name component. -Several of these rules have been taken from -https://chris.beams.io/posts/git-commit/#seven-rules. +[^original-commit-rules]: + Several of these rules have been taken from + https://chris.beams.io/posts/git-commit/#seven-rules. From 59e5ca9dde5546726ecf351c79dd5adb6a653654 Mon Sep 17 00:00:00 2001 From: Wolfgang Jeltsch Date: Tue, 23 Jan 2024 18:26:00 +0200 Subject: [PATCH 12/12] Fix copyright and licensing information --- LICENSE | 202 +++++++++++++++++++++++++++++++++++ LICENSE.md | 12 --- NOTICE | 2 + src/Equivalence_Reasoner.thy | 14 +++ 4 files changed, 218 insertions(+), 12 deletions(-) create mode 100644 LICENSE delete mode 100644 LICENSE.md create mode 100644 NOTICE diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..d645695 --- /dev/null +++ b/LICENSE @@ -0,0 +1,202 @@ + + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/LICENSE.md b/LICENSE.md deleted file mode 100644 index ede9826..0000000 --- a/LICENSE.md +++ /dev/null @@ -1,12 +0,0 @@ -Copyright 2022 IO Global - -Licensed under the Apache License, Version 2.0 (the “License”); you may -not use this repository or software bundle except in compliance with the -License. You may obtain a copy of the License at -https://www.apache.org/licenses/LICENSE-2.0. - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an “AS IS” BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. diff --git a/NOTICE b/NOTICE new file mode 100644 index 0000000..6fb1dfe --- /dev/null +++ b/NOTICE @@ -0,0 +1,2 @@ +equivalence-reasoner +Copyright 2021–2024 Input Output Global Inc. diff --git a/src/Equivalence_Reasoner.thy b/src/Equivalence_Reasoner.thy index 03d4306..2425ba7 100644 --- a/src/Equivalence_Reasoner.thy +++ b/src/Equivalence_Reasoner.thy @@ -1,3 +1,17 @@ +(* + Copyright 2021–2024 Input Output Global Inc. + + Licensed under the Apache License, Version 2.0 (the “License”); you may not use this file except + in compliance with the License. You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software distributed under the License + is distributed on an “AS IS” BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express + or implied. See the License for the specific language governing permissions and limitations under + the License. +*) + section \Introduction\ text \