search

emina / rosette

The Rosette solver-aided host language, sample solver-aided DSLs, and demos
Other
638 stars 74 forks source link

solvers: avoid specifying solver paths in define-runtime-path #278

Open sorawee opened 6 months ago

sorawee commented 6 months ago

On commands like raco distribute, paths under define-runtime-path will be copied over for distribution, which mandates their existence. Therefore, we should only use define-runtime-path with paths that we know for sure that they exist.

gussmith23 commented 6 months ago

FWIW, putting the solver binaries into Rosette did turn out to be the cleanest way to package up my project. It eliminated the need for extra logic telling Rosette where the packaged solvers are. I wouldn't have discovered this feature without Rosette forcing the binaries to be present. I do think that making the binaries optional is definitely the right idea, though perhaps there should be some specific documentation on packaging up projects that use Rosette, specifically suggesting that copying the binaries into Rosette is an easy route to packaging up the binaries.