Yeah, I really should use it... I think I mostly haven't because our build scripts don't, and I'm not sure why that is (IIRC it's hard to automate or something? Or was?).
Conversation
To automate this, I fear you'll need a `prepare-profiles.sh` and a build script relying on those envs. Plus pain when prepare-profiles.sh changes, unless you can detect which build profiles exist (which you probably can?)...
I'd prefer this to what you describe but YMMV!
2
1
I am now scared and want to run away to Lean again... but yes, I want to run this stuff on CI and this would be neccessary. And I hate dev config being in READMEs 🤦♂️
1
yikes wait, does ``eval `opam config env` `` mutate your shell state?
1
Probably... not sure why else eval would be used here.
1
Yeah, guess I'm just used to the cargo/npm/yarn/bundler approach of working off the current directory and config files. Just seems quite easy to forget that you've altered your environment in a long running shell.
1
It just sets environment vars (PATH etc.) — use `opam config env` to see what it'll do. New shells get that automatically (once you add that command to the init sequence) — but opam switch *sets* the default profile, so you're scared of the wrong thing IMHO? :-D
1
1
Ah, right, gotcha. Can you pin stuff scoped to a specific directory?
2
I don't know and I wouldn't, but it sounds like you're coming at a '90s build tool with expectations from the 2020s.
Right now, to *play* with autosubst, I'm modifying the examples in a checkout. And later I'd "vendor" it (paste it in my tree), it's not fast-moving :-)
1
1
I admire your resolve, but my current *feeling* is that investigating this would be lots of yak-shaving—and in a domain, binding lemmas, which is a YUGE YAK itself!
1
1
Hehe, sorry, you are right! It's pretty late here too, so I should get some rest!


