agda 2.7.0.1

Author: pthariensflame

Formula/a/agda.rb

@@ -4,21 +4,31 @@ class Agda < Formula
   # agda2hs.cabal specifies BSD-3-Clause but it installs an MIT LICENSE file.
   # Everything else specifies MIT license and installs corresponding file.
   license all_of: ["MIT", "BSD-3-Clause"]
-  revision 2
 
   stable do
-    url "https://github.com/agda/agda/archive/refs/tags/v2.6.4.3-r1.tar.gz"
-    sha256 "15a0ebf08b71ebda0510c8cad04b053beeec653ed26e2c537614a80de8b2e132"
-    version "2.6.4.3"
+    url "https://github.com/agda/agda/archive/refs/tags/v2.7.0.1.tar.gz"
+    sha256 "4a2c0a76c55368e1b70b157b3d35a82e073a0df8f587efa1e9aa8be3f89235be"
 
     resource "stdlib" do
-      url "https://github.com/agda/agda-stdlib/archive/refs/tags/v2.1.tar.gz"
-      sha256 "72ca3ea25094efa0439e106f0d949330414232ec4cc5c3c3316e7e70dd06d431"
+      url "https://github.com/agda/agda-stdlib/archive/refs/tags/v2.2.tar.gz"
+      sha256 "588f94af7fedd5aa1a6a1f0afdfb602d3e4615c7a17e6a0ae9dff326583b7a12"
+
+      # Backport support for building with GHC 9.12
+      patch do
+        url "https://github.com/agda/agda-stdlib/commit/a78700653de116b1043ce5d80bbe99482a705ecc.patch?full_index=1"
+        sha256 "547af4793368a7b37d7b707cc25d0b87bab674233ed69d38d4d685c28e574a58"
+      end
     end
 
     resource "cubical" do
       url "https://github.com/agda/cubical/archive/refs/tags/v0.7.tar.gz"
       sha256 "25a0d1a0a01ba81888a74dfe864883547dbc1b06fa89ac842db13796b7389641"
+
+      # Bump Agda compat
+      patch do
+        url "https://github.com/agda/cubical/commit/6220641fc7c297a84c5e2c49614fae518cf6307d.patch?full_index=1"
+        sha256 "c6919e394ac9dc6efa016fa6b4e9163ce58142d48f7100b6bc354678fc982986"
+      end
     end
 
     resource "categories" do
@@ -35,8 +45,8 @@ class Agda < Formula
     end
 
     resource "agda2hs" do
-      url "https://github.com/agda/agda2hs/archive/refs/tags/v1.2.tar.gz"
-      sha256 "e80ffc90ff2ccb3933bf89a39ab16d920a6c7a7461a6d182faa0fb6c0446dbb8"
+      url "https://github.com/agda/agda2hs/archive/refs/tags/v1.3.tar.gz"
+      sha256 "0e2c11eae0af459d4c78c24efadb9a4725d12c951f9d94da4adda5a0bcb1b6f6"
     end
   end
 
@@ -86,37 +96,30 @@ class Agda < Formula
 
   def install
     agda2hs = buildpath/"agda2hs"
-    agdalib = lib/"agda"
+    agdalib = pkgshare # for write permissions needed to re-generate .agdai when using different options
     cubicallib = agdalib/"cubical"
     categorieslib = agdalib/"categories"
 
+    # Add a backwards compatibility symlink. Can consider removing in a future release
+    lib.install_symlink pkgshare
+
     resource("agda2hs").stage agda2hs
     resource("stdlib").stage agdalib
     resource("cubical").stage cubicallib
     resource("categories").stage categorieslib
 
-    # Backport part of https://github.com/agda/agda-stdlib/commit/a78700653de116b1043ce5d80bbe99482a705ecc
-    inreplace agdalib/"agda-stdlib-utils.cabal", /( base .*) < 4\.21$/, "\\1 < 4.22" if build.stable?
+    # Remove strict stdlib version check in categories
+    inreplace categorieslib/"agda-categories.agda-lib", /(standard-library)-2\.1$/, "\\1", audit_result: build.stable?
 
     (buildpath/"cabal.project.local").write <<~HASKELL
       packages: . #{agda2hs}
       package Agda
         flags: +optimise-heavily
+      -- Workaround for GHC 9.12 until official supported, https://github.com/agda/agda/issues/7574
+      allow-newer: Agda:base, agda2hs:base, agda2hs:filepath
     HASKELL
 
-    cabal_args = std_cabal_v2_args
-    # Workaround for GHC 9.12 until official support is available
-    # Issue ref: https://github.com/agda/agda/issues/7574
-    cabal_args += %w[
-      --allow-newer=Agda:base
-      --allow-newer=agda2hs:base
-      --allow-newer=agda2hs:filepath
-    ]
-    # Workaround for https://github.com/agda/agda/commit/e11ae9875470aab7b68b98d9d9574e736dbcaddd
-    if build.stable?
-      odie "Remove allow-newer hashable workaround!" if version > "2.6.4.3"
-      cabal_args << "--allow-newer=Agda:hashable"
-    end
+    cabal_args = std_cabal_v2_args.map { |s| s.sub "=copy", "=symlink" }
     # Reduce install size by dynamically linking to shared libraries in store-dir
     # TODO: Linux support, related issue https://github.com/haskell/cabal/issues/9784
     cabal_args += %w[--enable-executable-dynamic --enable-shared] if OS.mac?
@@ -161,12 +164,12 @@ module Everything where
 
     # write out the example libraries and defaults files for users to copy
     (agdalib/"example-libraries").write <<~TEXT
-      #{opt_lib}/agda/standard-library.agda-lib
-      #{opt_lib}/agda/doc/standard-library-doc.agda-lib
-      #{opt_lib}/agda/tests/standard-library-tests.agda-lib
-      #{opt_lib}/agda/cubical/cubical.agda-lib
-      #{opt_lib}/agda/categories/agda-categories.agda-lib
-      #{opt_lib}/agda/agda2hs/agda2hs.agda-lib
+      #{opt_pkgshare}/standard-library.agda-lib
+      #{opt_pkgshare}/doc/standard-library-doc.agda-lib
+      #{opt_pkgshare}/tests/standard-library-tests.agda-lib
+      #{opt_pkgshare}/cubical/cubical.agda-lib
+      #{opt_pkgshare}/categories/agda-categories.agda-lib
+      #{opt_pkgshare}/agda2hs/agda2hs.agda-lib
     TEXT
     (agdalib/"example-defaults").write <<~TEXT
       standard-library
@@ -181,20 +184,20 @@ def caveats
       To use the installed Agda libraries, execute the following commands:
 
           mkdir -p $HOME/.config/agda
-          cp #{opt_lib}/agda/example-libraries $HOME/.config/agda/libraries
-          cp #{opt_lib}/agda/example-defaults $HOME/.config/agda/defaults
+          cp #{opt_pkgshare}/example-libraries $HOME/.config/agda/libraries
+          cp #{opt_pkgshare}/example-defaults $HOME/.config/agda/defaults
 
       You can then inspect the copied files and customize them as needed.
     EOS
   end
 
   test do
-    Pathname("#{Dir.home}/.config/agda").install_symlink opt_lib/"agda/example-libraries" => "libraries"
-    Pathname("#{Dir.home}/.config/agda").install_symlink opt_lib/"agda/example-defaults" => "defaults"
+    Pathname("#{Dir.home}/.config/agda").install_symlink opt_pkgshare/"example-libraries" => "libraries"
+    Pathname("#{Dir.home}/.config/agda").install_symlink opt_pkgshare/"example-defaults" => "defaults"
 
     simpletest = testpath/"SimpleTest.agda"
     simpletest.write <<~AGDA
-      {-# OPTIONS --safe --without-K #-}
+      {-# OPTIONS --safe --cubical-compatible #-}
       module SimpleTest where
 
       infix 4 _≡_
@@ -266,6 +269,7 @@ module IOTest where
     agda2hstest = testpath/"Agda2HsTest.agda"
     agda2hstest.write <<~AGDA
       {-# OPTIONS --erasure #-}
+      module Agda2HsTest where
       open import Haskell.Prelude
 
       _≤_ : {{Ord a}} → a → a → Set
@@ -302,9 +306,8 @@ module Agda2HsTest where
     # compile a simple module using the JS backend
     system bin/"agda", "--js", simpletest
 
-    # test the GHC backend;
-    # compile and run a simple program
-    system bin/"agda", "--ghc-flag=-fno-warn-star-is-type", "--compile", iotest
+    # test the GHC backend; compile and run a simple program
+    system bin/"agda", "--compile", iotest
     assert_empty shell_output(testpath/"IOTest")
 
     # translate a simple file via agda2hs