Nix flake installation option

[panther03]

Changes:

• Add a flake.nix giving users the option to set up a semi-isolated environment that installs the necessary system and OCaml dependencies to build and run OptiTrust (works with the interactive stuff that uses the browser as well)
• Update the INSTALL.md to document setting this up
• Also update the versions of the OCaml packages mentioned in INSTALL.md, since it currently calls for versions that are no longer available. Nix flake also installs these newer packages

TODOs:

• Figure out how to install libcxx-15 in nix - can't find a nix package that works and it seems it was working for me before only because I had it on my Ubuntu host.
• Review against Bastian nix flake local changes (if its not fixing the above)
  • had to eliminate libc++ from flags and stdlibc++ from nix flake to use system stdlibc++ instead
• Bastian double check that direnv instructions in readme works
  • using host vscode doesnt work to begin with through nix shell for him, but maybe this would still work
• Deal with other host/nix libc conflicts? browsers people have installed? Other utils needed to run the editor scripts like xdotool?

[Bastacyclop]

have you tried this thing ? https://search.nixos.org/packages?channel=unstable&show=llvmPackages.libcxxClang&query=llvmPackages

[bastian-koepcke]

I am on arch linux with glibc 2.42+r33+gde1fe81f4714-1 and code installed via the package repository.

executing

nix develop
code .

leads to a linker error with electron/code, which is linked against my system library.

I assume that your system glibc and the version downloaded and set via flake.nix are the same for you. This would explain why you can run code?

I made optitrust work for me by removing pkgs.gcc.cc.lib from the inputs in flake.nix (and therefore not settting LD_LIBRARY_PATH either) and by removing dependency on libc++ in include/Makefile and tools/c_parser/c_parser.ml. I do not think that this is necessarily a long term or general solution.

Would it make sense to alternatively bundle a VS code version with flake.nix, if possible? Or is it safe to remove the dependency on libc++?

[panther03]

I am on arch linux with glibc 2.42+r33+gde1fe81f4714-1 and code installed via the package repository.

executing

nix develop
code .

leads to a linker error with electron/code, which is linked against my system library.

I assume that your system glibc and the version downloaded and set via flake.nix are the same for you. This would explain why you can run code?

Bummer, OK I probably should not have assumed code was not going to work so easily. I tested it on Arch so I figured things would be fine but I'm technically on the WSL version so it's actually using the windows version of the IDE/electron internally.

I made optitrust work for me by removing pkgs.gcc.cc.lib from the inputs in flake.nix (and therefore not settting LD_LIBRARY_PATH either) and by removing dependency on libc++ in include/Makefile and tools/c_parser/c_parser.ml. I do not think that this is necessarily a long term or general solution.

OK. It's up to @charguer , who added the libc++ in the first place. He changed it because Clang searching for a GCC installation for the stdlib would lead to unpredictable results. Maybe an alternative is to just specify what version of GCC you need to at least have installed (not necessarily default), and change the flag passed in c_parser to reflect that?

It's interesting though that you had to remove pkgs.gcc.cc.lib, that means for whatever reason your system libstdc++ works and the Nix one doesn't.. I'm guessing the nix package is too old because this is all on Nix 22.XX.

Would it make sense to alternatively bundle a VS code version with flake.nix, if possible? Or is it safe to remove the dependency on libc++?

Well, these are two separate questions - see above for the libc++. Bundling VS Code could get tricky (and clunky) very quick. It's nice if it can run on the host because you can use all of your existing settings, can be launched from the desktop with Direnv, etc. At this point we'd probably just want to cover our bases and have the browser installed in Nix as well. I think all the watcher stuff would still work but yeah it would just make the workflow a little annoying. We could make it slightly less bad by providing an "install script" that installs some desktop entries for the "OptiTrust IDE" (special version of vscode launched thru nix shell). But of course currently that nix environment is tied to the repo itself so that probably won't work well either.

Convenience issues aside (since I appreciate there is huge functionality missing from the nix environment still), the version of VSCode that's provided and works in the Nix might be too ancient for some features we need. Specifically, I'm thinking the change we made some time ago to support the new tasks mechanism would have to be undone. Maybe the watcher script would break. I'm not sure. New extensions may not even support being installed on such an old version anymore. I don't think we want to split our userbase into a group of people who are able to running a version of VSCode from 3 years ago and another group who can run the newest version. Only reason I think we should consider an ancient VSCode setup is if there's like an appimage type thing where we can say 'this is the OptiTrust IDE running on VSCode internally, it has all the deps bundled' and we force everyone to use that. À la Vitis HLS or Arduino IDE powered by VSCode internally. If we go in that direction Nix may not even make sense. I think AppImage does things differently.

It's not so important for the vscode/electron binary itself to be running on the Nix. Hell, on my desktop these are running on Windows, I just have the WSL SSH to handle everything else. There are just three things I can think that we need to run on Nix:

1. The OPAM commands executed by the tasks
2. opam commands run in the terminal by the user
3. OCaml LSP (needs to point to the Nix environment, not the one on the host).
   The Nix environment sets up a local opam repo in the repository. Maybe a system opam/ocaml lsp can read this ? Depends on how deep the libc dependencies run.

TL;DR see the original post I've edited for the problems we still have to solve. Here are some questions/decisions for us to think about, in terms of solving them. Some are much more long term than others and we don't need to decide immediately just may help us save more work in the future:

• Do we want to mandate libc++ for everyone, switch to stdlibc++ with a specific version for everyone, do one thing for host-side users and one for nix users, or just go back to the old method where it pulled whatever? Is there a way to say 'try libc++ if it is installed, otherwise do stdlibc++, instead of failing'? The pro of libc++ is that it's unambiguous how to get a matching version, just get an LLVM that matches it. The only con of libc++ is it's not clear how to get it in the Nix yet (see my reply to @Bastacyclop comment below). And I think @Bastacyclop might have had problems getting libc++-15 on 24.04 and had to just use the stdlibc++ anyway? Or did I misremember?
• Is using the Nix 2022 version of VSCode acceptable? In general, if we figure out how to pin everything to a newer NixOS packages (maybe possible, I just gave up because getting our other deps to run on newer stdlibc++ was a mess), is fixing any version of VSCode acceptable? Note that it will use the same config files as the host - having a different set of extensions on one version that touches the same files as the other might get very messy.
• Do we want to explore alternative sandboxing solutions like Docker? Personally I still have a lot of doubts this will work with the stuff we need like the watcher, browser, etc. because it's actually sandboxed unlike Nix (Nix is just managing paths; access to the kernel resources works identically basically). But maybe it simplifies the dependency hell/conflicts with the host.
• What's the long term vision for the OptiTrust UI? Do we plan on supporting other editors - not bothering to do the tasks & scripts for other editors ourself, but say an Emacs user comes along and does a PR we would accept it? Or is the vision, especially as we refine the interactivity of OptiTrust, to be a very editor specific thing, instead of most of it being a browser interface? I imagine if we do the former while supporting other editors, we are going to have a Rocq like situation with proof general, vscode-rocq, etc. all being nontrivial things to maintain separately, which is probably beyond our capacity. Wondering if @charguer has experience/lessons from the Rocq world
• If the answer to the above is that everything will be VSCode specific, and not happening in the browser, how do we feel about a VSCode fork "OptiTrust IDE" like Arduino?
• Do we envision needing an isolated environment like Nix as a pretty temporary thing, because we eventually plan to switch to a pretty standard set of ocaml dependencies once we eliminate clangml and make our own parser? And then it will be reasonable for everyone to install stuff on their system?
• Will OptiTrust development always happen in-repo? Do we plan on supporting people writing scripts & transfos in their own repo with OptiTrust as a dependency of some kind, or is the solution always to fork? Just asking because this may dictate whether a per-repo Nix and opam environment would make sense

And finally @bastian-koepcke, can you summarize what it is you're missing to have a comfortable workflow? Do you have a way to use the LSP in Ocaml? Is launching nix develop each time from the terminal in VSCode acceptable? Can we just add some hacks for workarounds for your system?

I ask because you are our only user that needs this at the moment so I think it makes sense to split this PR into two steps - the minimal we need for Bastian to have a comfortable workflow, that we can merge so he can base his work off, and then the 'proper' environment solution. We can consider getting rid of the documentation in this PR or suggesting it as a very experimental thing until we do part 2.

[panther03]

have you tried this thing ? https://search.nixos.org/packages?channel=unstable&show=llvmPackages.libcxxClang&query=llvmPackages

I have. For whatever reason I don't think it installs the headers, only the libraries. Maybe I missed something, but I looked at the package that it installed in the nix store and it was nowhere to be found. It certainly wasnt auto detected by the clang I had installed. I probably have because it seems weird that there would be no way to get the header files through Nix.

[panther03]

I am on arch linux with glibc 2.42+r33+gde1fe81f4714-1 and code installed via the package repository.

executing

nix develop
code .

leads to a linker error with electron/code, which is linked against my system library.

I assume that your system glibc and the version downloaded and set via flake.nix are the same for you. This would explain why you can run code?

I made optitrust work for me by removing pkgs.gcc.cc.lib from the inputs in flake.nix (and therefore not settting LD_LIBRARY_PATH either) and by removing dependency on libc++ in include/Makefile and tools/c_parser/c_parser.ml. I do not think that this is necessarily a long term or general solution.

Would it make sense to alternatively bundle a VS code version with flake.nix, if possible? Or is it safe to remove the dependency on libc++?

Oh one other thing - you may not be able to launch the IDE through the host, but perhaps you could try my direnv solution (I've added instructions to in INSTALL.md in this branch)? This would just reload certain parts of the IDE like the extensions & etc. with the Nix stuff in the path. This may avoid dealing with libc conflicts for Electron cuz I think it runs on host either way, and I reckon this would be a good enough solution even relatively long term if it works.

[charguer]

the libc++ in the first place
If you find a reliable way to install a Nix package without libc++ but using gcc headers instead, it's perfectly fine to just use a flag to control 'include/Makefile' and 'c_parser.ml' behavior to include or not the --libc++ compiler flag.

[charguer]

What's the long term vision for the OptiTrust UI? Wondering if @charguer has experience/lessons from the Rocq world

Experience is that maintaining more than one UI is too much effort for a research team. My policy is: (1) we support VScode ; (2) we try to make it not infeasible for users who insist on using emacs/vim to adapt the bindings.

To achieve (2), I use bash scripts to implement all actions. The VScode bindings trigger basic calls to these bash scripts. The rendering is performed in a webpage using a server that is independent of VScode.

In the long term, someone might want to integrate into VScode the browser window and the associated server; however a few years ago VScode did not yet have the feature for detaching tabs to separate screens, which we do need. The benefits of having a VScode integration is to avoid the dependency on the X-server and xdotools, both of which require deactivating Wayland on Ubuntu.

[charguer]

We would like to maintain a Nix package in the long term, so that students can easily play with OptiTrust, in particular in the context of compiler courses, or for summer schools and tutorials that would teach OptiTrust.

[charguer]

Obviously we need at some point people to be able to use OptiTrust on scripts that live outside our repo. But we said this was not yet a top priority. Besides, we need first to introduce a version numbering system, so that scripts can indicate which version of OptiTrust (or even of each transformation) they depend upon. Nontrivial design is needed there. The aim is to do better than the usual 'everything gets broken behind your back at every single release'.

[charguer]

You can try docker if you think it would work better. The fact that we go through a watch.sh script for issueing commands, and through a webserver for answering queries, means that, assuming your server port in open, you should be able to escape your bocker sandbox. But this might take some effort.

[panther03]

I had a chat with Bastian, it would be great for him if we can merge this into main so he doesn't need to copy over the nix flake into his working branch each time. Since it's still an experimental thing, I updated the docs again to add a disclaimer. @Bastacyclop @charguer Let me know if we can merge this