jesper-bengtson / charge Goto Github PK

Remove reference to MirrorCore.TCLemma since it is moved into MirrorCore.Lemma on the "reify-func-no-table" branch of mirrorcore, which is the one that should work with this branch. The files in question are: Charge/Rewriter/BIlogicRewrite.v and Charege/Rewriter/ILogicRewriter.v

It is a little bit annoying to see so many warnings about paths when building the system.

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.

This seems like a really strange place to prove that String is an OrderedType. None of the rest of the file depends on this definition.

Also, concerning the same file, but a different part. What are the extra lemmas at the end of the file for? I would have expected this file to end by proving that [Map [K,V]] is a SeparationAlgebra. Are these extra properties useful for proving things in other files? If so, does that mean that SepAlg is not a complete definition?

Currently coqtop is started from the eclipse folder, it would probably make more sense to start it from the project folder. I am open to suggestions.

This fails to parse

Notation "'{xml:' e '>'" := e.
Eval simpl in {xml:5>.

Notation "'<xml:' e '>'" := e.
Eval simpl in xml:5.

This parses successfully.

Notation "'{xml:' e '}'" := e.
Eval simpl in {xml:5}.

Notation "'<xml:' e '}'" := e.
Eval simpl in <xml:5}.

We need definitions of 'pure' that work well with all separation logics (classical and intuitionistic). The (current) <-> definition that I proposed originally doesn't work, as Jesper pointed out so we need to go back and change it and prove all of the relevant lemmas for /, /, ->, etc for all of the ways that we build BI logics.

I can volunteer to do this.

Can Charge! be built under a library name to prevent name collisions with other projects?

Here is a patch

diff --git a/Charge!/KopitiamMakefile b/Charge!/KopitiamMakefile
index 342d76d..d3d5a71 100644
--- a/Charge!/KopitiamMakefile
+++ b/Charge!/KopitiamMakefile
@@ -4,11 +4,8 @@ COQFLAGS = -noglob

 bin/%.vo: src/%.v
        $(_COQCMD)
-override COQFLAGS += -R "src" ""
-override COQFLAGS += -R "bin" ""
-override COQFLAGS += -R "/Users/jebe/coqs/coq-8.4pl2/theories" "Coq"
-override COQFLAGS += -R "/Users/jebe/coqs/coq-8.4pl2/plugins" "Coq"
-override COQFLAGS += -R "/Users/jebe/coqs/coq-8.4pl2/user-contrib" ""
+override COQFLAGS += -R "src" -as "Charge"
+override COQFLAGS += -R "bin" -as "Charge"
 OBJECTS = \
        bin/Logics/BILInsts.vo \
        bin/Logics/BILogic.vo \