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

idris2: init at version 0.2.0-840e020 #88645

Merged
merged 1 commit into from May 26, 2020
Merged

idris2: init at version 0.2.0-840e020 #88645

merged 1 commit into from May 26, 2020

Conversation

wchresta
Copy link
Member

@wchresta wchresta commented May 23, 2020 •
edited

A purely functional programming language with first class types

Motivation for this change

Add a new derivation for Idris2, the successor of Idris.

This is my first new derivation. It does not have the fancy infrastructure that idris or haskell have, and it does not add any of the tooling that should be there. But I figured it's better than nothing.

I'm more than happy to edit this to support best practices, if anyone has suggestions.

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.

@Mic92
Copy link
Member

Mic92 commented May 23, 2020

Since idris2 does not yet have the ecosystem of idris1 (package manager etc), its too early to provide the same infrastructure yet.

@doronbehar doronbehar mentioned this pull request May 23, 2020
Closed
10 tasks
@wchresta wchresta force-pushed the master branch 2 times, most recently from a7946ec to 188d105 Compare May 23, 2020 16:30
wchresta
wchresta commented May 23, 2020
View reviewed changes
pkgs/development/compilers/idris2/default.nix
patchShebangs --build tests

# Do not run tests as part of the build process
substituteInPlace bootstrap.sh --replace "make test" "# make test"
Copy link
Member Author

Choose a reason for hiding this comment

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

I added this because the build script of Idris2 does an automatic test. As far as I can tell, it's not common to run tests after builds, so I deactivated them.

I havn't found a good way to reproduce the test command as a separate phase, since it depends on a few paths that seem only to be available in the script.

I wanted to keep this derivation as close to the intended build process, since I suspect it's going to change, and I don't want to spend a lot of time rewriting this derivation every-time it happens.

Any suggestions welcome.

Copy link
Member

Choose a reason for hiding this comment

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

I think I'd personally prefer running the tests as part of the build phase to not running them at all. Maybe upstream would be amenable to making bootstrap.sh take a phase to run (e.g. stage1, stage2, test) so that this could be split out into checkPhase without duplicating the script's logic?

Copy link
Member Author

Choose a reason for hiding this comment

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

I added an upstream feature request to separate building from testing: idris-lang/Idris2#125

@wchresta
idris2: init at version 0.2.0-840e020
074c9cb 
A purely functional programming language with first class types
@wchresta wchresta requested a review from Mic92 May 23, 2020 17:03
@emilazy
Copy link
Member

emilazy commented May 23, 2020

There's also the option to bootstrap via Idris 1 with Idris2-boot rather than using the pre-generated compiler output in the repository. Not worth blocking the package for, but maybe a note could be added for future work?

@wchresta
Copy link
Member Author

wchresta commented May 23, 2020 •
edited

There's also the option to bootstrap via Idris 1 with Idris2-boot rather than using the pre-generated compiler output in the repository. Not worth blocking the package for, but maybe a note could be added for future work?

I thought about compiling idris2-boot as you suggested, but that would involve building -> idris -> idris2-boot -> idris2 which seems less optimal than precompiled scheme -> idris-boot -> idris2 since it has more dependencies and will also take significantly longer, I'd assume.

I'm open to be convinced that we should indeed go the idris2-boot route, instead; if there's good reasons not to use the current scheme way. Both ways seem to be rather flaky, since they both depend on either the pre-generated scheme or idris2-boot being kept up-to-date.

@emilazy
Copy link
Member

emilazy commented May 23, 2020

Keeping in line with the general preference to build from source over using binaries, it's nicest to bootstrap from a source form where possible rather than having to rely on third-party compiler output. Reasons include mitigating Reflections on Trusting Trust attacks, and generally ensuring as pure, hermetic, and reproducible a build environment for nixpkgs as possible rather than bringing in the "unaccounted-for externality" of the output of someone else's compiler run.

However, it's true that in this case that involves bootstrapping through Haskell and the previous version of the language, which would be slow and involve a lot of build-time dependencies. The best thing in the long run is probably to offer an option to turn off the full bootstrap; Hydra can leave it on and share the result via the binary caches, but people doing development on the compiler who want faster builds could switch it off.

Again, though, it might be some fuss to get this wired up fully so I don't mean to imply I think this should all be done in this PR ^^ Just a future direction to consider.

@wchresta wchresta mentioned this pull request May 23, 2020
Closed
@wchresta wchresta removed the request for review from Mic92 May 24, 2020 22:56
@fabianhjr
Copy link
Member

fabianhjr commented May 25, 2020 •
edited

Hi @wchresta, v0.2.0 has been released (Announcement: https://www.idris-lang.org/idris-2-version-020-released.html), you might want to change this PR.

Also, this PR supersedes #76971 which should be closed.

@Mic92 Mic92 mentioned this pull request May 25, 2020
Closed
10 tasks
@Mic92
Copy link
Member

Mic92 commented May 26, 2020

Keeping in line with the general preference to build from source over using binaries, it's nicest to bootstrap from a source form where possible rather than having to rely on third-party compiler output. Reasons include mitigating Reflections on Trusting Trust attacks, and generally ensuring as pure, hermetic, and reproducible a build environment for nixpkgs as possible rather than bringing in the "unaccounted-for externality" of the output of someone else's compiler run.

However, it's true that in this case that involves bootstrapping through Haskell and the previous version of the language, which would be slow and involve a lot of build-time dependencies. The best thing in the long run is probably to offer an option to turn off the full bootstrap; Hydra can leave it on and share the result via the binary caches, but people doing development on the compiler who want faster builds could switch it off.

Again, though, it might be some fuss to get this wired up fully so I don't mean to imply I think this should all be done in this PR ^^ Just a future direction to consider.

Afaik our ghc is build from pre-compiled binaries while chez is built with only a C compiler, which means that we rely on less boot binaries using the scheme version for now.

@Mic92
Copy link
Member

Mic92 commented May 26, 2020

Result of nixpkgs-review pr 88645 1

1 package built:
- idris2

@Mic92 Mic92 merged commit f76f13b into NixOS:master May 26, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Mic92 Mic92 Mic92 left review comments

@emilazy emilazy emilazy left review comments

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

Successfully merging this pull request may close these issues.

None yet
4 participants
@wchresta @Mic92 @emilazy @fabianhjr