Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

agdarsec: init at 0.4.1 #100351

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

agdarsec: init at 0.4.1 #100351

wants to merge 2 commits into from

Conversation

@turion
Copy link
Contributor

@turion turion commented Oct 12, 2020

Motivation for this change

Add the https://github.com/gallais/agdarsec/ library to nixpkgs
u

Things done
  • Tested using sandboxing (nix.useSandbox on NixOS, or option sandbox in nix.conf on non-NixOS linux)
  • Built on platform(s)
    • NixOS
    • macOS
    • other Linux distributions
  • Tested via one or more NixOS test(s) if existing and applicable for the change (look inside nixos/tests)
  • Tested compilation of all pkgs that depend on this change using nix-shell -p nixpkgs-review --run "nixpkgs-review wip"
  • Tested execution of all binary files (usually in ./result/bin/)
  • Determined the impact on package closure size (by running nix path-info -S before and after)
  • Ensured that relevant documentation is up to date
  • Fits CONTRIBUTING.md.

@alexarice

@turion
Copy link
Contributor Author

@turion turion commented Oct 12, 2020

I'm currently having trouble to build:

nix-repl> :b agdaPackages.agdarsec
builder for '/nix/store/bwfq8fswhs2l9a65zkh9yranhpv331q5-agdarsec-v0.3.0.drv' failed with exit code 1; last 10 log lines:
  building
  Checking index (/build/source/index.agda).
   Checking Text.Parser.Types (/build/source/src/Text/Parser/Types.agda).
   Checking Text.Parser.Combinators (/build/source/src/Text/Parser/Combinators.agda).
    Checking Induction.Nat.Strong (/build/source/src/Induction/Nat/Strong.agda).
    Checking Data.List.Any (/nix/store/vrr50yf58l2k36vw9clm43hfahn7msfh-standard-library-1.3/src/Data/List/Any.agda).
  Failed to write interface /nix/store/vrr50yf58l2k36vw9clm43hfahn7msfh-standard-library-1.3/src/Data/List/Any.agdai.
  /build/source/src/Text/Parser/Combinators.agda:17,8-28
  /nix/store/vrr50yf58l2k36vw9clm43hfahn7msfh-standard-library-1.3/src/Data/List/Any.agdai:
  openBinaryFile: permission denied (Permission denied)
[0 built (1 failed)]
error: build of '/nix/store/bwfq8fswhs2l9a65zkh9yranhpv331q5-agdarsec-v0.3.0.drv' failed

Strangely, it wants to recheck standard library files. Any idea why it might want to do that? Maybe agdarsec changes some build flag in a way that causes recompilation?

@alexarice
Copy link
Contributor

@alexarice alexarice commented Oct 12, 2020

I think this suggests that something in standard library is not being compiled

@turion
Copy link
Contributor Author

@turion turion commented Oct 12, 2020

@alexarice You're right!

$ ls /nix/store/vrr50yf58l2k36vw9clm43hfahn7msfh-standard-library-1.3/src/Data/List/Any.*
/nix/store/vrr50yf58l2k36vw9clm43hfahn7msfh-standard-library-1.3/src/Data/List/Any.agda
$ cat /nix/store/vrr50yf58l2k36vw9clm43hfahn7msfh-standard-library-1.3/Everything.agda | grep List.Any
-- Data.List.Any.Membership instantiated with propositional equality,

It seems the everything file is generated incorrectly.

@alexarice
Copy link
Contributor

@alexarice alexarice commented Oct 12, 2020

See https://github.com/agda/agda-stdlib/blob/master/src/Data/List/Any.agda.

The issue is that agdarsec relies on a deprecated module in standard library, and deprecated modules aren't built. Likely agdarsec needs updating to use the undeprecated module

@turion
Copy link
Contributor Author

@turion turion commented Oct 12, 2020

Hah. After monkey-patching Data.List.Any into the everything file, I get:

$ nix repl .
Welcome to Nix version 2.3.7. Type :? for help.

Loading '.'...
Added 12573 variables.

nix-repl> :b agdaPackages.agdarsec
builder for '/nix/store/qa9hmr88h2ib9zc5qf06kb909a1mqibd-standard-library-1.3.drv' failed with exit code 1; last 10 log lines:
    Checking Text.Tabular.Vec (/build/source/src/Text/Tabular/Vec.agda).
   Checking Text.Tree.Linear (/build/source/src/Text/Tree/Linear.agda).
   Checking Data.List.Any (/build/source/src/Data/List/Any.agda).
  /build/source/Everything.agda:1985,1-21
  Data.List.Any was deprecated in v1.0.
  Use Data.List.Relation.Unary.Any instead.
  when scope checking the declaration
    import Data.List.Any

So it's actually a deprecation warning.

@turion
Copy link
Contributor Author

@turion turion commented Oct 12, 2020

@alexarice Yes, right. This is fixed on master I think.

@AndersonTorres AndersonTorres marked this pull request as draft Oct 13, 2020
@AndersonTorres
Copy link
Member

@AndersonTorres AndersonTorres commented Oct 13, 2020

@turion do you think it is a good idea to use master, then?

@turion
Copy link
Contributor Author

@turion turion commented Oct 13, 2020

@AndersonTorres It would be ok in principle until the next release, but unfortunately master doesn't work out of the box either because of version mismatches. I'm working on a workaround.

pkgs/development/libraries/agda/agdarsec/default.nix Outdated Show resolved Hide resolved
pkgs/applications/editors/vscode/vscodium.nix Outdated Show resolved Hide resolved
@turion
Copy link
Contributor Author

@turion turion commented Nov 29, 2020

I'm currently stuck on this error:

nix-repl> :b agdaPackages.agdarsec
builder for '/nix/store/djhsxg2av3g3wdvbcimq29dj0j602hkf-agdarsec-v0.3.0.drv' failed with exit code 1; last 10 log lines:
    /nix/store/1b7jp08xlcbvankbf8aml162zmid00la-standard-library-1.4/src/Expr.agda
    /nix/store/1b7jp08xlcbvankbf8aml162zmid00la-standard-library-1.4/src/Expr.lagda
    /build/source/src/Expr.agda
    /build/source/src/Expr.lagda
    /build/source/Expr.agda
    /build/source/Expr.lagda
    /nix/store/vkm07q5a493h356zmlqzvn7sxc4r0wwv-Agda-2.6.1.2-data/share/ghc-8.10.2/x86_64-linux-ghc-8.10.2/Agda-2.6.1.2/lib/prim/Expr.agda
    /nix/store/vkm07q5a493h356zmlqzvn7sxc4r0wwv-Agda-2.6.1.2-data/share/ghc-8.10.2/x86_64-linux-ghc-8.10.2/Agda-2.6.1.2/lib/prim/Expr.lagda
  when scope checking the declaration
    import Expr
[1 built (1 failed), 0.0 MiB DL]
error: build of '/nix/store/djhsxg2av3g3wdvbcimq29dj0j602hkf-agdarsec-v0.3.0.drv' failed

See gallais/agdarsec#21.

@turion turion force-pushed the dev_add_agdarsec branch from 8d08a07 to 76118da Nov 29, 2020
@turion turion force-pushed the dev_add_agdarsec branch from 76118da to 39768d6 Feb 5, 2021
@turion turion marked this pull request as ready for review Feb 5, 2021
@turion
Copy link
Contributor Author

@turion turion commented Feb 5, 2021

@alexarice @neosimsim do you want to have a look? I also extended the build support a little. Now you can add the -i option (include paths) through nix.

@turion
Copy link
Contributor Author

@turion turion commented Feb 5, 2021

@ofborg build agdaPackages.agdarsec
@ofborg test agdaPackages.standard-library.passthru.tests

@turion turion requested a review from SuperSandro2000 Feb 15, 2021
@turion
Copy link
Contributor Author

@turion turion commented Feb 15, 2021

@ofborg build agdaPackages.agdarsec
@ofborg test agdaPackages.standard-library.passthru.tests

@turion turion force-pushed the dev_add_agdarsec branch from 39768d6 to 4ee7a81 Feb 15, 2021
@turion
Copy link
Contributor Author

@turion turion commented Feb 15, 2021

@ofborg build agdaPackages.agdarsec
@ofborg test agdaPackages.standard-library.passthru.tests

@stale
Copy link

@stale stale bot commented Aug 15, 2021

I marked this as stale due to inactivity. → More info

@turion turion force-pushed the dev_add_agdarsec branch from 4ee7a81 to 93a2010 Aug 17, 2021
@stale stale bot removed the 2.status: stale label Aug 17, 2021
@turion
Copy link
Contributor Author

@turion turion commented Aug 17, 2021

@ofborg build agdaPackages.agdarsec
@ofborg build agdaPackages.standard-library.passthru.tests

@turion
Copy link
Contributor Author

@turion turion commented Aug 17, 2021

@alexarice @SuperSandro2000 fine like this?

@alexarice
Copy link
Contributor

@alexarice alexarice commented Aug 17, 2021

Looks fine to me. I'm surprised we haven't hit the include path problem before. Maybe we should do things like include the stdlib readmes? (this an be a separate pr)

@nixos-discourse
Copy link

@nixos-discourse nixos-discourse commented Aug 17, 2021

This pull request has been mentioned on NixOS Discourse. There might be relevant details there:

https://discourse.nixos.org/t/prs-already-reviewed/2617/397

@AndersonTorres AndersonTorres changed the title Dev add agdarsec agdarsec: init at 0.4.1 Aug 20, 2021
@turion turion force-pushed the dev_add_agdarsec branch from 24e48a3 to 2e5ce89 Aug 30, 2021
@turion turion requested a review from SuperSandro2000 Aug 30, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Linked issues

Successfully merging this pull request may close these issues.

None yet

5 participants