jesper-bengtson / charge Goto Github PK
View Code? Open in Web Editor NEWHigher-order separation logic framework in Coq
License: Other
Higher-order separation logic framework in Coq
License: Other
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 \
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.