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

Jump to bottom

agdarsec: init at 0.4.1 #100351

Merged
merged 2 commits into from Oct 6, 2021
Merged

agdarsec: init at 0.4.1 #100351

merged 2 commits into from Oct 6, 2021

Conversation

turion
Copy link
Contributor

@turion turion commented Oct 12, 2020 •
edited

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 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

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

@turion
Copy link
Contributor Author

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.

@ofborg ofborg bot requested a review from Synthetica9 October 12, 2020 18:15
@alexarice
Copy link
Contributor

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 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 commented Oct 12, 2020

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

@AndersonTorres AndersonTorres marked this pull request as draft October 13, 2020 03:38
@AndersonTorres
Copy link
Member

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

@turion
Copy link
Contributor Author

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.

@turion turion mentioned this pull request Nov 29, 2020
Closed
@turion
Copy link
Contributor Author

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 marked this pull request as ready for review February 5, 2021 16:04
@turion
Copy link
Contributor Author

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 commented Feb 5, 2021

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

@ofborg ofborg bot added the 6.topic: agda label Feb 5, 2021
@turion turion requested a review from alexarice February 5, 2021 16:07
@turion turion closed this Feb 12, 2021
@turion turion reopened this Feb 12, 2021
@turion
Copy link
Contributor Author

turion commented Feb 15, 2021

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

@turion
Copy link
Contributor Author

turion commented Feb 15, 2021

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

@stale
Copy link

stale bot commented Aug 15, 2021

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

@stale stale bot added the 2.status: stale https://github.com/NixOS/nixpkgs/blob/master/.github/STALE-BOT.md label Aug 15, 2021
@stale stale bot removed the 2.status: stale https://github.com/NixOS/nixpkgs/blob/master/.github/STALE-BOT.md label Aug 17, 2021
@turion
Copy link
Contributor Author

turion commented Aug 17, 2021

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

@turion
Copy link
Contributor Author

turion commented Aug 17, 2021

@alexarice @SuperSandro2000 fine like this?

@alexarice
Copy link
Contributor

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

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
Copy link
Contributor Author

turion commented Oct 6, 2021

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

@turion
Copy link
Contributor Author

turion commented Oct 6, 2021

@SuperSandro2000 Are you fine with the changes?

SuperSandro2000
SuperSandro2000 reviewed Oct 6, 2021
View reviewed changes
Copy link
Member

@SuperSandro2000 SuperSandro2000 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have no clue about agda but I did not see anything which is worth a comment.

@AndersonTorres AndersonTorres merged commit d3ee4ba into NixOS:master Oct 6, 2021
@turion turion deleted the dev_add_agdarsec branch October 7, 2021 10:07
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@SuperSandro2000 SuperSandro2000 SuperSandro2000 requested changes

@Synthetica9 Synthetica9 Awaiting requested review from Synthetica9

@alexarice alexarice Awaiting requested review from alexarice

Assignees
No one assigned
Labels
6.topic: agda 8.has: package (new) 10.rebuild-darwin: 1-10 10.rebuild-linux: 1-10 11.by: package-maintainer
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@turion @alexarice @AndersonTorres @nixos-discourse @SuperSandro2000