add `nix` to ci

[quinn-dougherty]

i'm starting a branch on my fork for this.

one solution

cp hs-to-coq.yml hs-to-coq-nix.yml and replace stack-built executable with nix-built executable in hs-to-coq-nix.yml when it tests that examples work as expected, duplicating code (not ideal).

Another solution

breaking out into precheck.yml and calling that job from both hs-to-coq-stack.yml and hs-to-coq-nix.yml, to replicate the basic conditional logic about not running jobs if relevant files weren't edited. In general, it's possible that a .yml file well under 430 lines would be easier to reason about.

galaxybrained best solution?

a stack process and a nix process each build an executable, and those two executables are input to one job sequence, which runs once for the stack-built executable and once for the nix-built executable. I don't know how to do this, off the top of my head.

passing in a ghcVersion argument to .nix should be a pretty easy way for the nix side of ci to improve upon the https://github.com/plclub/hs-to-coq/issues/200 situation.

[lastland]

I am not familiar with the nix workflow so I can't comment which one works best, but it does seem helpful to split the current CI script into some reusable modules.

[quinn-dougherty]

I thought of that. I can piggyback splitting up the main ci file into multiple files (but retain identical functionality) into a PR that has nix ci. However, the pipeline view (attached) is based on files, so there are advantages to having one 400 line ci file. But I would hope there's some way to retain the view you want even if there are multiple files. For example, if there's hs-to-coq-stack.yml and hs-to-coq-nix.yml they should each import precheck.yml instead of each of them starting with duplicated precheck jobs. It's probably desirable for nix and stack ci to be on different pipeline views.