From 4e427e2e5117d4976fc22e20362d01fbed9c6679 Mon Sep 17 00:00:00 2001 From: Lex Bailey Date: Sat, 30 Mar 2024 02:15:29 +0000 Subject: [PATCH 1/3] CI --- .github/workflows/build_2021-1.yml | 15 --------------- .github/workflows/build_2022.yml | 16 ---------------- .github/workflows/build_2023.yml | 16 ++++++++++++++++ 3 files changed, 16 insertions(+), 31 deletions(-) delete mode 100644 .github/workflows/build_2021-1.yml delete mode 100644 .github/workflows/build_2022.yml create mode 100644 .github/workflows/build_2023.yml diff --git a/.github/workflows/build_2021-1.yml b/.github/workflows/build_2021-1.yml deleted file mode 100644 index e6b24f0..0000000 --- a/.github/workflows/build_2021-1.yml +++ /dev/null @@ -1,15 +0,0 @@ -on: [push] -jobs: - build: - runs-on: ubuntu-latest - name: Build Theory - steps: - - uses: actions/checkout@v3 - - uses: lexbailey/isabelle-theory-build-github-action@v7 - with: - isabelle-version: '2021-1' - custom-isabelle-url: 'https://github.com/lexbailey/itrees_isabelle_fork/archive/refs/tags/itrees_utp_2021-1.zip' - depends: 'https://github.com/isabelle-utp/Shallow-Expressions.git@main https://github.com/isabelle-utp/explore-subgoal.git@main' - session-name: 'Interaction_Trees ITree_Simulation ITree_UTP ITree_VCG ITree_RoboChart' - report_url: 'https://isabelle-utp-ci-dashboard.link/submit_job_log' - report_secret: ${{ secrets.DashboardReportKey }} diff --git a/.github/workflows/build_2022.yml b/.github/workflows/build_2022.yml deleted file mode 100644 index 26955a7..0000000 --- a/.github/workflows/build_2022.yml +++ /dev/null @@ -1,16 +0,0 @@ -on: [push] -jobs: - build: - runs-on: ubuntu-latest - name: Build Theory - steps: - - uses: actions/checkout@v3 - - uses: lexbailey/isabelle-theory-build-github-action@v7 - with: - isabelle-version: '2022' - custom-isabelle-url: 'https://github.com/lexbailey/itrees_isabelle_fork/archive/refs/heads/itrees_utp_2022.zip' - depends: 'https://github.com/isabelle-utp/Shallow-Expressions.git@main https://github.com/isabelle-utp/explore-subgoal.git@main' - session-name: 'Interaction_Trees ITree_Simulation ITree_UTP ITree_VCG ITree_RoboChart' - report_url: 'https://isabelle-utp-ci-dashboard.link/submit_job_log' - report_secret: ${{ secrets.DashboardReportKey }} - diff --git a/.github/workflows/build_2023.yml b/.github/workflows/build_2023.yml new file mode 100644 index 0000000..e384844 --- /dev/null +++ b/.github/workflows/build_2023.yml @@ -0,0 +1,16 @@ +on: [push] +jobs: + build: + runs-on: ubuntu-latest + name: Build Theory + steps: + - uses: actions/checkout@v3 + - uses: lexbailey/isabelle-theory-build-github-action@v9 + with: + isabelle-url: 'https://github.com/lexbailey/itrees_isabelle_fork/archive/refs/tags/CyPhyAssure2023.tar.gz' + depends: 'https://github.com/lexbailey/Shallow-Expressions.git@main https://github.com/lexbailey/explore-subgoal.git@main https://github.com/lexbailey/Abstract_Prog_Syntax.git@main' + session-name: 'Interaction_Trees ITree_Simulation ITree_UTP ITree_VCG ITree_RoboChart' + report_url: 'https://isabelle-utp-ci-dashboard.link/submit_job_log' + report_secret: ${{ secrets.DashboardReportKey }} + + From c144f76ed42ed547a0c74cdb1296e07119111e22 Mon Sep 17 00:00:00 2001 From: Lex Bailey Date: Mon, 29 Apr 2024 14:00:04 +0100 Subject: [PATCH 2/3] added some useful lemmas to ITree_Relation --- UTP/ITree_Relation.thy | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/UTP/ITree_Relation.thy b/UTP/ITree_Relation.thy index 85d10ca..51c4201 100644 --- a/UTP/ITree_Relation.thy +++ b/UTP/ITree_Relation.thy @@ -101,6 +101,13 @@ lemma promote_rel [itree_pred]: by (auto elim!: trace_to_bindE bind_RetE' simp add: itree_pred_def retvals_def promote_itree_def lens_override_def) (metis bind_Ret trace_to_bind_left) +lemma itree_pred_match [simp]: + "match_itree (e)\<^sub>e (case_option P Q) = (if e = None then P else (let v \ the e in Q v) fi)" + by (simp add: match_itree_def let_itree_def cond_itree_def option.case_eq_if fun_eq_iff) + +lemma let_itree_pred [itree_pred]: "\let_itree e P\\<^sub>p = (\ (s, s'). let v = e s in \P v\\<^sub>p (s, s'))" + by (simp add: let_itree_def itree_pred_def) + ML_file \Lens_Rel_Utils.ML\ method rename_rel_alpha_vars = tactic \ Lens_Rel_Utils.rename_rel_alpha_vars \ From 5acb194063c8b73005d1563989fb606bce939c0b Mon Sep 17 00:00:00 2001 From: Lex Bailey Date: Mon, 29 Apr 2024 15:34:13 +0100 Subject: [PATCH 3/3] switch to using isabelle-utp repos for CI --- .github/workflows/build_2023.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/build_2023.yml b/.github/workflows/build_2023.yml index e384844..e0f2184 100644 --- a/.github/workflows/build_2023.yml +++ b/.github/workflows/build_2023.yml @@ -8,7 +8,7 @@ jobs: - uses: lexbailey/isabelle-theory-build-github-action@v9 with: isabelle-url: 'https://github.com/lexbailey/itrees_isabelle_fork/archive/refs/tags/CyPhyAssure2023.tar.gz' - depends: 'https://github.com/lexbailey/Shallow-Expressions.git@main https://github.com/lexbailey/explore-subgoal.git@main https://github.com/lexbailey/Abstract_Prog_Syntax.git@main' + depends: 'https://github.com/isabelle-utp/Shallow-Expressions.git@main https://github.com/isabelle-utp/explore-subgoal.git@main https://github.com/isabelle-utp/Abstract_Prog_Syntax.git@main' session-name: 'Interaction_Trees ITree_Simulation ITree_UTP ITree_VCG ITree_RoboChart' report_url: 'https://isabelle-utp-ci-dashboard.link/submit_job_log' report_secret: ${{ secrets.DashboardReportKey }}