FStar icon indicating copy to clipboard operation
FStar copied to clipboard

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

Open shonfeder opened this issue 1 year ago • 1 comments
trafficstars

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.

shonfeder avatar Dec 08 '23 18:12 shonfeder

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.

mtzguido avatar Dec 08 '23 22:12 mtzguido