Tracking issue: trivialBuild should retire in favor of melpaBuild #278925

AndersonTorres · 2024-01-05T13:06:30Z

Describe the bug

According to @jian-lin the trivialBuild function has some problems that make it a bad fit for Emacs ecosystem in Nixpkgs.

In packages made via trivialBuild:

The builtin package manager package.el will not activate it at the Emacs' startup
- autoloaded commands does not work out-of-the-box, requiring bolierplate code like (require 'foo-autoloads)
- info manual becomes inaccessible viaM-x info
its package dir is not searched by Emacs
it does not contain a foo-pkg.el file

References:

emacsPackages.codeium: init at 1.6.13 #278201 (comment)

Add a 👍 reaction to issues you find important.

The text was updated successfully, but these errors were encountered:

jian-lin · 2024-01-05T14:17:54Z

I think we should:

make reviewers and contributors aware that trivialBuild has some issues and its usage is discouraged
replace existing trivialBuild in manual-packages with melpaBuild or elpaBuild

AndersonTorres · 2024-01-05T15:03:32Z

We should do this in reverse: first by looking at current code that uses trivialBuild, and only then to warn new devs.

I say this because I remember some packages fail with melpaBuild. I didn't know how to use it with sunrise-commander

AndersonTorres · 2024-01-05T16:08:42Z

Example: I have tried to update sunrise-commander:

{ lib
, elpaBuild
, fetchFromGitHub
, emacs
}:

elpaBuild {
  pname = "sunrise-commander";
  ename = "sunrise-commander";
  version = "unstable-2021-09-27";

  src = fetchFromGitHub {
    owner = "sunrise-commander";
    repo = "sunrise-commander";
    rev = "16e6df7e86c7a383fb4400fae94af32baf9cb24e";
    hash = "sha256-D36qiRi5OTZrBtJ/bD/javAWizZ8NLlC/YP4rdLCSsw=";
  };

  packageRequires = [
    emacs
  ];

  meta = {
    homepage = "https://github.com/sunrise-commander/sunrise-commander/";
    description = "Orthodox (two-pane) file manager for Emacs";
    license = lib.licenses.gpl3Plus;
    maintainers = [ lib.maintainers.AndersonTorres ];
    platforms = lib.platforms.all;
  };
}

The error log:

emacs-sunrise-commander-unstable> Running phase: installPhase
emacs-sunrise-commander-unstable> Error: file-error ("Read error" "Is a directory" "/nix/store/da7c3cm3m6m0in0c6d28m25r2qc585b5-source")
emacs-sunrise-commander-unstable>   mapbacktrace(#f(compiled-function (evald func args flags) #<bytecode -0xcc6be0a6510e41>))
emacs-sunrise-commander-unstable>   debug-early-backtrace()
emacs-sunrise-commander-unstable>   debug-early(error (file-error "Read error" "Is a directory" "/nix/store/da7c3cm3m6m0in0c6d28m25r2qc585b5-source"))
emacs-sunrise-commander-unstable>   insert-file-contents("/nix/store/da7c3cm3m6m0in0c6d28m25r2qc585b5-source")
emacs-sunrise-commander-unstable>   (if is-tar (insert-file-contents-literally file) (insert-file-contents file))
emacs-sunrise-commander-unstable>   (progn (if is-tar (insert-file-contents-literally file) (insert-file-contents file)) (if is-tar (progn (tar-mode))) (elpa2nix-install-from-buffer))
emacs-sunrise-commander-unstable>   (unwind-protect (progn (if is-tar (insert-file-contents-literally file) (insert-file-contents file)) (if is-tar (progn (tar-mode))) (elpa2nix-install-from-buffer)) (and (buffer-name temp-buffer) (kill-buffer temp-buffer)))
emacs-sunrise-commander-unstable>   (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (if is-tar (insert-file-contents-literally file) (insert-file-contents file)) (if is-tar (progn (tar-mode))) (elpa2nix-install-from-buffer)) (and (buffer-name temp-buffer) (kill-buffer temp-buffer))))
emacs-sunrise-commander-unstable>   (let ((temp-buffer (generate-new-buffer " *temp*" t))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (if is-tar (insert-file-contents-literally file) (insert-file-contents file)) (if is-tar (progn (tar-mode))) (elpa2nix-install-from-buffer)) (and (buffer-name temp-buffer) (kill-buffer temp-buffer)))))
emacs-sunrise-commander-unstable>   (let ((is-tar (string-match "\\.tar\\'" file))) (let ((temp-buffer (generate-new-buffer " *temp*" t))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (if is-tar (insert-file-contents-literally file) (insert-file-contents file)) (if is-tar (progn (tar-mode))) (elpa2nix-install-from-buffer)) (and (buffer-name temp-buffer) (kill-buffer temp-buffer))))))
emacs-sunrise-commander-unstable>   elpa2nix-install-file("/nix/store/da7c3cm3m6m0in0c6d28m25r2qc585b5-source")
emacs-sunrise-commander-unstable>   (progn (setq package-user-dir elpa) (elpa2nix-install-file archive))
emacs-sunrise-commander-unstable>   (let ((archive x0) (elpa x2)) (progn (setq package-user-dir elpa) (elpa2nix-install-file archive)))
emacs-sunrise-commander-unstable>   (if (null x3) (let ((archive x0) (elpa x2)) (progn (setq package-user-dir elpa) (elpa2nix-install-file archive))))
emacs-sunrise-commander-unstable>   (let* ((x2 (car-safe x1)) (x3 (cdr-safe x1))) (if (null x3) (let ((archive x0) (elpa x2)) (progn (setq package-user-dir elpa) (elpa2nix-install-file archive)))))
emacs-sunrise-commander-unstable>   (if (consp x1) (let* ((x2 (car-safe x1)) (x3 (cdr-safe x1))) (if (null x3) (let ((archive x0) (elpa x2)) (progn (setq package-user-dir elpa) (elpa2nix-install-file archive))))))
emacs-sunrise-commander-unstable>   (let* ((x0 (car-safe command-line-args-left)) (x1 (cdr-safe command-line-args-left))) (if (consp x1) (let* ((x2 (car-safe x1)) (x3 (cdr-safe x1))) (if (null x3) (let ((archive x0) (elpa x2)) (progn (setq package-user-dir elpa) (elpa2nix-install-file archive)))))))
emacs-sunrise-commander-unstable>   (if (consp command-line-args-left) (let* ((x0 (car-safe command-line-args-left)) (x1 (cdr-safe command-line-args-left))) (if (consp x1) (let* ((x2 (car-safe x1)) (x3 (cdr-safe x1))) (if (null x3) (let ((archive x0) (elpa x2)) (progn (setq package-user-dir elpa) (elpa2nix-install-file archive))))))))
emacs-sunrise-commander-unstable>   elpa2nix-install-package()
emacs-sunrise-commander-unstable>   command-line-1(("-l" "/nix/store/4jj63z4v1xp13rh2md053dccq920hd45-elpa2nix.el" "-f" "elpa2nix-install-package" "/nix/store/da7c3cm3m6m0in0c6d28m25r2qc585b5-source" "/nix/store/mv5i7kvw8m1siga6g3n6avbh0qzk71nz-emacs-sunrise-commander-unstable-2021-09-27/share/emacs/site-lisp/elpa"))
emacs-sunrise-commander-unstable>   command-line()
emacs-sunrise-commander-unstable>   normal-top-level()
emacs-sunrise-commander-unstable> Read error: Is a directory, /nix/store/da7c3cm3m6m0in0c6d28m25r2qc585b5-source
error: builder for '/nix/store/qzdqqh8dfy63jdnhm4n06x0pv97ap53i-emacs-sunrise-commander-unstable-2021-09-27.drv' failed with exit code 255;

jian-lin · 2024-01-05T16:14:59Z

elpaBuild expects src to be an elisp file or a tarball meeting some requirements. The requirement of src of melpaBuild is less strict than the one of elpaBuild.

Have you tried melpaBuild?

AndersonTorres · 2024-01-05T16:44:59Z

I tried it a long time ago. But let's do it again:

{ lib
, emacs
, fetchFromGitHub
, melpaBuild
, writeText
}:

melpaBuild {
  pname = "sunrise-commander";
  ename = "sunrise-commander";
  version = "unstable-2021-09-27";

  src = fetchFromGitHub {
    owner = "sunrise-commander";
    repo = "sunrise-commander";
    rev = "16e6df7e86c7a383fb4400fae94af32baf9cb24e";
    hash = "sha256-D36qiRi5OTZrBtJ/bD/javAWizZ8NLlC/YP4rdLCSsw=";
  };

  packageRequires = [
    emacs
  ];

  recipe = writeText "recipe" ''
    (sunrise-commander :repo "sunrise-commander/sunrise-commander" :fetcher github :files ("*.el"))
  '';

  fileSpecs = [ "*.el" ];

  meta = {
    homepage = "https://github.com/sunrise-commander/sunrise-commander/";
    description = "Orthodox (two-pane) file manager for Emacs";
    license = lib.licenses.gpl3Plus;
    maintainers = [ lib.maintainers.AndersonTorres ];
    platforms = lib.platforms.all;
  };
}

Log:

emacs-sunrise-commander-unstable> Running phase: installPhase
emacs-sunrise-commander-unstable> Error: file-missing ("Opening input file" "No such file or directory" "/build/packages/sunrise-commander-unstable-2021-09-27.tar")
emacs-sunrise-commander-unstable>   mapbacktrace(#f(compiled-function (evald func args flags) #<bytecode -0xcc6be0a6510e41>))
emacs-sunrise-commander-unstable>   debug-early-backtrace()
emacs-sunrise-commander-unstable>   debug-early(error (file-missing "Opening input file" "No such file or directory" "/build/packages/sunrise-commander-unstable-2021-09-27.tar"))
emacs-sunrise-commander-unstable>   insert-file-contents-literally("/build/packages/sunrise-commander-unstable-2021-09-27.tar")
emacs-sunrise-commander-unstable>   (if is-tar (insert-file-contents-literally file) (insert-file-contents file))
emacs-sunrise-commander-unstable>   (progn (if is-tar (insert-file-contents-literally file) (insert-file-contents file)) (if is-tar (progn (tar-mode))) (elpa2nix-install-from-buffer))
emacs-sunrise-commander-unstable>   (unwind-protect (progn (if is-tar (insert-file-contents-literally file) (insert-file-contents file)) (if is-tar (progn (tar-mode))) (elpa2nix-install-from-buffer)) (and (buffer-name temp-buffer) (kill-buffer temp-buffer)))
emacs-sunrise-commander-unstable>   (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (if is-tar (insert-file-contents-literally file) (insert-file-contents file)) (if is-tar (progn (tar-mode))) (elpa2nix-install-from-buffer)) (and (buffer-name temp-buffer) (kill-buffer temp-buffer))))
emacs-sunrise-commander-unstable>   (let ((temp-buffer (generate-new-buffer " *temp*" t))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (if is-tar (insert-file-contents-literally file) (insert-file-contents file)) (if is-tar (progn (tar-mode))) (elpa2nix-install-from-buffer)) (and (buffer-name temp-buffer) (kill-buffer temp-buffer)))))
emacs-sunrise-commander-unstable>   (let ((is-tar (string-match "\\.tar\\'" file))) (let ((temp-buffer (generate-new-buffer " *temp*" t))) (save-current-buffer (set-buffer temp-buffer) (unwind-protect (progn (if is-tar (insert-file-contents-literally file) (insert-file-contents file)) (if is-tar (progn (tar-mode))) (elpa2nix-install-from-buffer)) (and (buffer-name temp-buffer) (kill-buffer temp-buffer))))))
emacs-sunrise-commander-unstable>   elpa2nix-install-file("/build/packages/sunrise-commander-unstable-2021-09-27.tar")
emacs-sunrise-commander-unstable>   (progn (setq package-user-dir elpa) (elpa2nix-install-file archive))
emacs-sunrise-commander-unstable>   (let ((archive x0) (elpa x2)) (progn (setq package-user-dir elpa) (elpa2nix-install-file archive)))
emacs-sunrise-commander-unstable>   (if (null x3) (let ((archive x0) (elpa x2)) (progn (setq package-user-dir elpa) (elpa2nix-install-file archive))))
emacs-sunrise-commander-unstable>   (let* ((x2 (car-safe x1)) (x3 (cdr-safe x1))) (if (null x3) (let ((archive x0) (elpa x2)) (progn (setq package-user-dir elpa) (elpa2nix-install-file archive)))))
emacs-sunrise-commander-unstable>   (if (consp x1) (let* ((x2 (car-safe x1)) (x3 (cdr-safe x1))) (if (null x3) (let ((archive x0) (elpa x2)) (progn (setq package-user-dir elpa) (elpa2nix-install-file archive))))))
emacs-sunrise-commander-unstable>   (let* ((x0 (car-safe command-line-args-left)) (x1 (cdr-safe command-line-args-left))) (if (consp x1) (let* ((x2 (car-safe x1)) (x3 (cdr-safe x1))) (if (null x3) (let ((archive x0) (elpa x2)) (progn (setq package-user-dir elpa) (elpa2nix-install-file archive)))))))
emacs-sunrise-commander-unstable>   (if (consp command-line-args-left) (let* ((x0 (car-safe command-line-args-left)) (x1 (cdr-safe command-line-args-left))) (if (consp x1) (let* ((x2 (car-safe x1)) (x3 (cdr-safe x1))) (if (null x3) (let ((archive x0) (elpa x2)) (progn (setq package-user-dir elpa) (elpa2nix-install-file archive))))))))
emacs-sunrise-commander-unstable>   elpa2nix-install-package()
emacs-sunrise-commander-unstable>   command-line-1(("-l" "/nix/store/4jj63z4v1xp13rh2md053dccq920hd45-elpa2nix.el" "-f" "elpa2nix-install-package" "/build/packages/sunrise-commander-unstable-2021-09-27.tar" "/nix/store/6gf924kvnbpjgf7mrwmm93ih5pcjpkrr-emacs-sunrise-commander-unstable-2021-09-27/share/emacs/site-lisp/elpa"))
emacs-sunrise-commander-unstable>   command-line()
emacs-sunrise-commander-unstable>   normal-top-level()
emacs-sunrise-commander-unstable> Opening input file: No such file or directory, /build/packages/sunrise-commander-unstable-2021-09-27.tar

jian-lin · 2024-01-06T09:13:07Z

Here is a working example:

ename and recipe need to be change to sunrise
version needs to be changed
commit needs to have a value for now

{ lib
, emacs
, fetchFromGitHub
, melpaBuild
, writeText
}:

melpaBuild {
  pname = "sunrise-commander";
  ename = "sunrise";
  version = "20210924.1620";

  src = fetchFromGitHub {
    owner = "sunrise-commander";
    repo = "sunrise-commander";
    rev = "16e6df7e86c7a383fb4400fae94af32baf9cb24e";
    hash = "sha256-D36qiRi5OTZrBtJ/bD/javAWizZ8NLlC/YP4rdLCSsw=";
  };

  # not sure whether it is still needed when a newer[1] package-build is used
  # [1]: https://github.com/NixOS/nixpkgs/pull/276943 is in the staging branch for now
  commit = "foo";

  # probably redundant
  # packageRequires = [
  #   emacs
  # ];

  recipe = writeText "recipe" ''
    (sunrise :repo "sunrise-commander/sunrise-commander" :fetcher github)
  '';

  meta = {
    homepage = "https://github.com/sunrise-commander/sunrise-commander/";
    description = "Orthodox (two-pane) file manager for Emacs";
    license = lib.licenses.gpl3Plus;
    maintainers = [ lib.maintainers.AndersonTorres ];
    platforms = lib.platforms.all;
  };
}

AndersonTorres · 2024-01-06T13:29:03Z

Nice. Now we need to wait the Staging Truckload.

Where did the attribute version = "20210924.1620"; come from?
I have grepped the installed files and it comes from nowhere except an autogenerated sunrise-pkg.el...
What does fileSpecs do? It is not documented anywhere...

jian-lin · 2024-01-06T13:50:51Z

#190746 is related

jian-lin · 2024-01-06T13:59:00Z

Where did the attribute version = "20210924.1620"; come from?

This is the version format MELPA unstable uses.

(let ((time 1703448134))
  (concat (format-time-string "%Y%m%d." time t)
          (format "%d" (string-to-number
                        (format-time-string "%H%M" time t)))))

time is produced by a git command git log -n1 --first-parent --pretty='format:%H %cd' --date=unix.

I think fileSpecs has no effect since d3cea48#diff-2a37290b0927d8abb03148a01a10a84dd3a18be9be80d27c7aac6c02d8ea6841L14

Tracking issue #278925

AndersonTorres · 2024-01-07T21:16:58Z

Some obvious findings:

The recipe format is described here: https://github.com/melpa/melpa#recipe-format
maybe it can be Nixified.

hraban · 2024-02-24T17:20:45Z

Thanks for your work on this, y'all! 🙌

jian-lin · 2024-05-31T09:57:25Z

I created #316107 to improve the UX of melpaBuild.

jian-lin · 2024-06-02T20:11:20Z

With #316726, the UX of melpaBuild should be on a par with elpaBuild and trivialBuild.

Given that it has fewer issues than trivialBuild and that its requirement for src is looser than elpaBuild, it should be recommended as the default builder for manual packages.

AndersonTorres · 2024-07-07T03:55:29Z

Now that it reached Master, we can restart!

hraban · 2024-07-15T07:24:34Z

How do you use melpaBuild to create very simple in-line packages?

          (e.trivialBuild {
            pname = "foo";
            version = "2024-07-15";
            src = builtins.toFile "foo.el" ''(defun foo-three () 3) (provide 'foo)'';
          })

I use this to create light-weight emacs plugins from my Nix config, it's a neat way to integrate the broader system config into Emacs.

jian-lin · 2024-07-17T22:14:03Z

EmacsWiki repacks (they should be dealt with separately):

@AndersonTorres What do you mean by "they should be dealt with separately"? Why and how?

AndersonTorres · 2024-07-18T01:51:39Z

It is better explained with an example:

Let's pick control-lock.

Webpage: https://www.emacswiki.org/emacs/ControlLock
Download page: https://www.emacswiki.org/emacs/download/control-lock.el

There is virtually no version control.

However, there is a backup at GitHub:

https://github.com/emacsmirror/emacswiki.org/blob/master/control-lock.el

My intention is to create a "package" for this EmacsWiki mirror and do something like files = ''("control-lock.el")''.

Related: NixOS/nixpkgs#278925

AndersonTorres · 2024-07-21T12:46:10Z

Another thing to be seen is the auto-update scripts.

jian-lin · 2024-07-21T14:36:17Z

Another thing to be seen is the auto-update scripts.

Since trivialBuild works well in that use case (autolaoding is not used by update-melpa.el) and users is unlikely to look at that file, it's fine to not change it to melpaBuild.

I am working on the last piece of this issue, i.e., writing doc for these builders.

UPDATE: I block my doc work on #330589. This is just a personal choice. If you want to write doc for the current builders, please feel free to do so.

AndersonTorres · 2024-07-21T17:36:12Z

I wasn't clear. I was talking about passthru.updateScript.

jian-lin · 2024-08-17T13:21:45Z

@AndersonTorres Could you switch mkDerivation to melpaBuild for cask?

AndersonTorres · 2024-08-22T01:26:22Z

Yes I can. However I will need to study cask a little bit, since Cask is a commandline app.

AndersonTorres · 2024-09-04T00:18:14Z

For now the only "non-conforming" packages are xapian-lite and cedille.
However Cedille is broken:

Broken due to Agda update. See

#129606 (comment).

AndersonTorres added 0.kind: bug 6.topic: emacs labels Jan 5, 2024

AndersonTorres mentioned this issue Jan 5, 2024

emacsPackages.codeium: init at 1.6.13 #278201

Merged

13 tasks

This comment was marked as outdated.

Sign in to view

AndersonTorres mentioned this issue Jan 6, 2024

convert elisp packages to melpaBuild #279195

Closed

13 tasks

nagy mentioned this issue Jan 7, 2024

emacs.pkgs.wat-mode: convert to melpaBuild #279365

Merged

13 tasks

jian-lin pushed a commit that referenced this issue Jan 7, 2024

emacs.pkgs.wat-mode: convert to melpaBuild

454a9d8

Tracking issue #278925

This was referenced Jan 7, 2024

emacs.pkgs.color-theme-solarized: convert to melpaBuild #279472

Closed

updater-emacs: use nixpkgs packages instead of pinned ones #280059

Closed

samueldr added the 5. scope: tracking Long-lived issue tracking long-term fixes or multiple sub-problems label Apr 23, 2024

This was referenced May 30, 2024

emacs.pkgs.consult-gh: convert to a new rec-less format #315934

Closed

emacs.pkgs.git-undo: convert to melpaBuild #315935

Closed

emacs.pkgs.evil-markdown: convert to melpaBuild #315936

Closed

emacs.pkgs.yes-no: convert to melpaBuild #315937

Closed

AndersonTorres mentioned this issue Jul 7, 2024

mini-treewide: use melpabuild in some Elisp packages #325168

Merged

13 tasks

AndersonTorres mentioned this issue Jul 18, 2024

emacswiki snippets: cleanup #328074

Merged

13 tasks

AndersonTorres changed the title ~~Tracking issue: trivialBuild should retire in favor of elpaBuild and friends~~ Tracking issue: trivialBuild should retire in favor of melpaBuild Jul 18, 2024

This was referenced Jul 19, 2024

lspce: 1.0.0-unstable-2024-02-03 -> 1.1.0-unstable-2024-07-13 #326981

Merged

emacsPackages.isearch-plus: trivialBuild -> melpaBuild #328466

Merged

emacsPackages.isearch-prop: trivialBuild -> melpaBuild #328468

Merged

kira-bruneau pushed a commit to kira-bruneau/nur-packages that referenced this issue Jul 19, 2024

emacsPackages.lsp-bridge: clean

2294034

Related: NixOS/nixpkgs#278925

AndersonTorres mentioned this issue Jul 21, 2024

emacsPackages: add updateScript's #329005

Merged

13 tasks

jian-lin mentioned this issue Jul 22, 2024

emacs updater: trivialBuild -> melpaBuild #329008

Merged

13 tasks

This was referenced Jul 24, 2024

emacsPackages: add updatescripts (packages maintained by @leungbk) #329670

Merged

emacsPackages.idris2-mode: updateScript #329673

Merged

jian-lin mentioned this issue Aug 17, 2024

emacsPackages.session-management-for-emacs: mkDerivation -> melpaBuild #335420

Merged

13 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Tracking issue: trivialBuild should retire in favor of melpaBuild #278925

Tracking issue: trivialBuild should retire in favor of melpaBuild #278925

AndersonTorres commented Jan 5, 2024 •

edited

Loading

jian-lin commented Jan 5, 2024

AndersonTorres commented Jan 5, 2024 •

edited

Loading

This comment was marked as outdated.

AndersonTorres commented Jan 5, 2024

jian-lin commented Jan 5, 2024 •

edited

Loading

AndersonTorres commented Jan 5, 2024

jian-lin commented Jan 6, 2024 •

edited

Loading

AndersonTorres commented Jan 6, 2024

jian-lin commented Jan 6, 2024

jian-lin commented Jan 6, 2024

AndersonTorres commented Jan 7, 2024

hraban commented Feb 24, 2024

jian-lin commented May 31, 2024

jian-lin commented Jun 2, 2024

AndersonTorres commented Jul 7, 2024

hraban commented Jul 15, 2024

jian-lin commented Jul 17, 2024

AndersonTorres commented Jul 18, 2024

AndersonTorres commented Jul 21, 2024

jian-lin commented Jul 21, 2024 •

edited

Loading

AndersonTorres commented Jul 21, 2024

jian-lin commented Aug 17, 2024

AndersonTorres commented Aug 22, 2024

AndersonTorres commented Sep 4, 2024

Broken due to Agda update. See

#129606 (comment).

Tracking issue: trivialBuild should retire in favor of melpaBuild #278925

Tracking issue: trivialBuild should retire in favor of melpaBuild #278925

Comments

AndersonTorres commented Jan 5, 2024 • edited Loading

Describe the bug

jian-lin commented Jan 5, 2024

AndersonTorres commented Jan 5, 2024 • edited Loading

This comment was marked as outdated.

AndersonTorres commented Jan 5, 2024

jian-lin commented Jan 5, 2024 • edited Loading

AndersonTorres commented Jan 5, 2024

jian-lin commented Jan 6, 2024 • edited Loading

AndersonTorres commented Jan 6, 2024

jian-lin commented Jan 6, 2024

jian-lin commented Jan 6, 2024

AndersonTorres commented Jan 7, 2024

hraban commented Feb 24, 2024

jian-lin commented May 31, 2024

jian-lin commented Jun 2, 2024

AndersonTorres commented Jul 7, 2024

hraban commented Jul 15, 2024

jian-lin commented Jul 17, 2024

AndersonTorres commented Jul 18, 2024

AndersonTorres commented Jul 21, 2024

jian-lin commented Jul 21, 2024 • edited Loading

AndersonTorres commented Jul 21, 2024

jian-lin commented Aug 17, 2024

AndersonTorres commented Aug 22, 2024

AndersonTorres commented Sep 4, 2024

Broken due to Agda update. See

#129606 (comment).

AndersonTorres commented Jan 5, 2024 •

edited

Loading

AndersonTorres commented Jan 5, 2024 •

edited

Loading

jian-lin commented Jan 5, 2024 •

edited

Loading

jian-lin commented Jan 6, 2024 •

edited

Loading

jian-lin commented Jul 21, 2024 •

edited

Loading