FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.7k stars 234 forks source link

cannot be installed via `opam pin` in `opam` sandboxes #3144

Open shonfeder opened 11 months ago

shonfeder commented 11 months ago

I have been trying to install HEAD (or other more recent releases not yet available on opam) in an opam switch. Due to way the build and installation is currently defined, the installation and build fails.

To reproduce:

dune init proj repro
cd repro/
git init
opam switch create . 4.14.0
dune build
opam pin add fstar --dev-repo -y

to get an error along these lines:


[ERROR] The compilation of fstar.2023.09.03~dev failed at "make PREFIX=/repro/_opam -j 7".

#=== ERROR while compiling fstar.2023.09.03~dev ===============================#
# context     2.1.5 | linux/x86_64 | ocaml-system.4.14.0 | pinned(git+https://github.com/FStarLang/FStar#6e20d76e09f66dc3eea5c40eac008ea1338ceef1)
# path        ~/repro/_opam/.opam-switch/build/fstar.2023.09.03~dev
# command     ~/.opam/opam-init/hooks/sandbox.sh build make PREFIX=/repro/_opam -j 7
# exit-code   2
# env-file    ~/.opam/log/fstar-232551-a0b055.env
# output-file ~/.opam/log/fstar-232551-a0b055.out
### output ###
#   DUNE BUILD
# Error: _build/log: Read-only file system
# make: *** [Makefile:23: fstar] Error 1

<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ λ build fstar 2023.09.03~dev
└─ 
┌─ The following changes have been performed
# <snip>
└─ 
[NOTE] Pinning command successful, but your installed packages may be out of sync.

The former state can be restored with:
    /usr/bin/opam switch import "/repro/_opam/.opam-switch/backup/state-20231208175407.export"

I have not yet tracked down exactly what is going on during the build/install causing the illegal file access a directory which it shouldn't have access to. But I have been able to come with an rough patch that moves the build and install just into dune, and resolves the problem: https://github.com/shonfeder/FStar/compare/master...pinnable

This patch allows pinning in a switch, e.g., via

opam pin git+https://github.com/shonfeder/Fstar.git#pinnable

This patch can (currently) be rebased on top of the trunk quite easily.

mtzguido commented 11 months ago

Hi Shon, thanks for the report! I suppose we may be forgetting to set a variable somewhere and that ends up being some external directory (or maybe I'm paranoid about that ever since I read https://github.com/ocaml/opam/issues/3316). I can take a look.

I suppose a top-level dune project file would be a good thing. Wondering what @tahina-pro thinks.