search

jesper-bengtson / Charge

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

Isolate class definitions? #4

Open gmalecha opened 10 years ago

gmalecha commented 10 years ago

This is just a suggestion looking for feedback on it.

Is it possible/desirable to isolate the class definitions from their instances and to pull apart any instances that are not dependent on each other?

This would increase parallelism in building and facilitate faster importing times in other projects.

jesper-bengtson commented 10 years ago

Yes, I have try do this as much as possible but we can absolutely be more precise about these sort of things.

We have ILogicInsts and BILInsts and similar files. Exactly what other things did you have in mind? Should we put the morphisms for ILogic in separate files for instance?

On 25 Nov 2013, at 14:42, Gregory Malecha notifications@github.com<mailto:notifications@github.com> wrote:

This is just a suggestion looking for feedback on it.

Is it possible/desirable to isolate the class definitions from their instances and to pull apart any instances that are not dependent on each other?

This would increase parallelism in building and facilitate faster importing times in other projects.

— Reply to this email directly or view it on GitHubhttps://github.com/jesper-bengtson/Charge/issues/4.

gmalecha commented 10 years ago

I forked the Charge! repository and am looking into it. I'm also looking at some of the duplication between Charge! and ExtLib and possibly factoring things out a little bit to make things a bit cleaner (for example the orders and the equivalences).

I will post again when things in that repository are in a stable state and either close this as a wontfix or suggest a few patches. How would you feel about introducing ExtLib as a dependency (for the non-logic stuff)? Also, what is the Open directory for?

jesper-bengtson commented 10 years ago

I'm fine with requiring ExtLib as a dependency if you want to use things from there for your development. This will be more or less needed anyway as I would really like what we are doing now to go into the Tactics-folder at the end of the day.

The Open-directory handles program variables. An open term is a term with free program variables, pretty much using an environment monad. I mentioned it in my talk. I'm up for suggestions how to do this better, but the upside of this approach is that we can take any construct from the Coq standard library and allow it to reason about program variables.

/Jesper

On 26 Nov 2013, at 07:32, Gregory Malecha notifications@github.com<mailto:notifications@github.com> wrote:

I forked the Charge! repository and am looking into it. I'm also looking at some of the duplication between Charge! and ExtLib and possibly factoring things out a little bit to make things a bit cleaner (for example the orders and the equivalences).

I will post again when things in that repository are in a stable state and either close this as a wontfix or suggest a few patches. How would you feel about introducing ExtLib as a dependency (for the non-logic stuff)? Also, what is the Open directory for?

— Reply to this email directly or view it on GitHubhttps://github.com/jesper-bengtson/Charge/issues/4#issuecomment-29292047.

gmalecha commented 10 years ago

I've pushed the start of this. Right now it is essentially just the class definitions and the instance definitions for Prop. See https://github.com/gmalecha/Charge/commit/efd3a4ab707345f4087feac52f2b06c659494699