search

jesper-bengtson / Charge

Higher-order separation logic framework in Coq
Other
1 stars 1 forks source link

make the build system work. #8

Closed gmalecha closed 9 years ago

gmalecha commented 9 years ago

This commit fixes the build system for Charge. I wasn't certain if you wanted the views in Charge.Tactics.Views or just Charge.Views. Feel free to move them.

gmalecha commented 9 years ago

One other thing that I thought of is that maybe the symlinks to other projects should be in the root directory instead of the Charge! directory. Would this integrate well with the Coqoon stuff or should we keep them in the Charge! directory?

jesper-bengtson commented 9 years ago

I’m not sure that the symlink stuff is a good match for Coqoon as they end up in the Eclipse projects. We’ll have to think on this a bit more but ideally I would just have the user insert the local paths somewhere.

/Jesper

On 05 Aug 2015, at 03:26, Gregory Malecha notifications@github.com<mailto:notifications@github.com> wrote:

One other thing that I thought of is that maybe the symlinks to other projects should be in the root directory instead of the Charge! directory. Would this integrate well with the Coqoon stuff or should we keep them in the Charge! directory?

— Reply to this email directly or view it on GitHubhttps://github.com/jesper-bengtson/Charge/pull/8#issuecomment-127812122.

gmalecha commented 9 years ago

That seems reasonable. We could look into how to use the COQPATH environment variables to set things up. My motivation behind this is to make it very easy for anyone to build Charge! without anything special. The other thing is that user-specific options should never be checked into the repository, e.g. /Users/jebe should never occur in any file anywhere. If we commit user-specific things then we will likely have a ton of churn when people commit their own configurations and every pull is going to end up with a conflict.

One option might be to have a small configure script that runs coqtop on files that have: "Require Import MirrorCore.ExprI." or something like that. And if it fails (because MirrorCore is not installed, it prompts the user for a path to overwrite the path in the configuration. Of course, we need a different configuration file so maybe we should have

_CoqFiles -- contains the list of all the .v files (checked in) _CoqPaths -- contains the library paths (not checked in) _CoqProject -- = _CoqPaths + _CoqFiles (not checked in) Makefile -- glues together _CoqPaths and _CoqFiles to build _CoqProject, and then builds using that. If _CoqPaths does not exist, then it runs the script, possibly trying the default symbolic links that I proposed but falling back to the user if things are not already set up.

Does that seem reasonable?

gmalecha commented 9 years ago

Did you want the Views inside of Tactics or directly under Charge?

gmalecha commented 9 years ago

This latest commit separates the user-specific configuration from the global configuration. The global configuration is stored in _CoqConfig and the Makefile and the user-specific configuration is stored in _CoqPath (not-checked in). Running make _CoqProject will combine these two files into an working _CoqProject file. When _CoqPath does not exist, _CoqProject is exactly the contents of _CoqConfig which is exactly what is needed to build this project with Opam.

This system seems very feasible for Coqoon to hook into. .v files that are added to the project should be placed at the end of _CoqConfig (or in sorted order). The options in _CoqConfig should be passed on the command line of coqtop and all of the Coqoon dependencies can be managed locally without polluting any checked in files (e.g. it could be stored in _CoqPath or anywhere else).

gmalecha commented 9 years ago

Rebased on top of 8.5