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

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 commented May 23, 2020

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
Contributor

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
4 of 10 tasks complete
@wchresta wchresta force-pushed the wchresta:master branch 2 times, most recently from a7946ec to 188d105 May 23, 2020
patchShebangs --build tests
# Do not run tests as part of the build process
substituteInPlace bootstrap.sh --replace "make test" "# make test"

This comment has been minimized.

Copy link
@wchresta

wchresta May 23, 2020

Author Member

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.

This comment has been minimized.

Copy link
@emilazy

emilazy May 23, 2020

Member

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?

This comment has been minimized.

Copy link
@wchresta

wchresta May 23, 2020

Author Member

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

A purely functional programming language with first class types
@wchresta wchresta force-pushed the wchresta:master branch from 188d105 to 074c9cb May 23, 2020
@wchresta wchresta requested a review from Mic92 May 23, 2020
@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

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 removed the request for review from Mic92 May 24, 2020
@fabianhjr
Copy link
Contributor

fabianhjr commented May 25, 2020

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
3 of 10 tasks complete
@Mic92
Copy link
Contributor

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
Contributor

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
16 checks passed
16 checks passed
idris2, idris2.passthru.tests on aarch64-linux No attempt
Details
Evaluation Performance Report Evaluator Performance Report
Details
grahamcofborg-eval ^.^!
Details
grahamcofborg-eval-check-maintainers matching changed paths to changed attrs...
Details
grahamcofborg-eval-check-meta config.nix: checkMeta = true
Details
grahamcofborg-eval-darwin nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="074c9cb"; rev="074c9cbe1cd42301c142401e0604d520bf3dae9f"; } ./pkgs/t
Details
grahamcofborg-eval-lib-tests nix-build --arg pkgs import ./. {} ./lib/tests/release.nix
Details
grahamcofborg-eval-nixos nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="074c9cb"; rev="074c9cbe1cd42301c142401e0604d520bf3dae9f"; } ./nixos/
Details
grahamcofborg-eval-nixos-manual nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="074c9cb"; rev="074c9cbe1cd42301c142401e0604d520bf3dae9f"; } ./nixos/
Details
grahamcofborg-eval-nixos-options nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="074c9cb"; rev="074c9cbe1cd42301c142401e0604d520bf3dae9f"; } ./nixos/
Details
grahamcofborg-eval-nixpkgs-manual nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="074c9cb"; rev="074c9cbe1cd42301c142401e0604d520bf3dae9f"; } ./pkgs/t
Details
grahamcofborg-eval-nixpkgs-tarball nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="074c9cb"; rev="074c9cbe1cd42301c142401e0604d520bf3dae9f"; } ./pkgs/t
Details
grahamcofborg-eval-nixpkgs-unstable-jobset nix-instantiate --arg nixpkgs { outPath=./.; revCount=999999; shortRev="074c9cb"; rev="074c9cbe1cd42301c142401e0604d520bf3dae9f"; } ./pkgs/t
Details
grahamcofborg-eval-package-list nix-env -qa --json --file .
Details
grahamcofborg-eval-package-list-no-aliases nix-env -qa --json --file . --arg config { allowAliases = false; }
Details
idris2, idris2.passthru.tests on x86_64-linux Success
Details
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

4 participants
You can’t perform that action at this time.