mit-plv / fiat Goto Github PK
View Code? Open in Web Editor NEWMostly Automated Synthesis of Correct-by-Construction Programs
Home Page: http://plv.csail.mit.edu/fiat/
License: Other
fiat's People
Contributors
![dependabot[bot] avatar](https://avatars.githubusercontent.com/in/29110?v=4 "dependabot[bot]")
Stargazers
Watchers
Forkers
jasongross ejgallego ppedrot maximedenes herbelin ilyasergey zimmi48 epsilonsolutions jashug skyskimmer bendy mattam82 simonboulier vbgl olaure01 llelf proux01 gares mrhaandi coqsucker pinkdiamond1 drruisseau villetaneusefiat's Issues
Fail to make querystructures on Coq > 8.9
I clone the repo and follow the instruction "make querystructures" to build the SQL-like library, but it fail, the error message is below
COQC src/QueryStructure/Specification/SearchTerms/ListInclusion.v
Warning: The -require option is deprecated, please use -require-import
instead. [deprecated-boot,deprecated]
File "./src/QueryStructure/Specification/SearchTerms/ListInclusion.v", line 49, characters 2-140:
Error: Unsolved obligations remaining.
Makefile.coq:677: recipe for target 'src/QueryStructure/Specification/SearchTerms/ListInclusion.vo' failed
make: *** [src/QueryStructure/Specification/SearchTerms/ListInclusion.vo] Error 1
my system is Ubuntu 16.04, my "coqc -v" output is
The Coq Proof Assistant, version 8.11.0 (March 2020)
compiled on Mar 23 2020 4:55:38 with OCaml 4.07.1
[Coq 8.9+] Please fix deprecation warnings in 8.9
Please fix deprecation warning in 8.9 so your plugin will compile with Coq 8.10, thanks!
CAMLOPT -c src/Common/Tactics/transparent_abstract_tactics.ml
File "src/Common/Tactics/transparent_abstract_tactics.ml", line 22, characters 57-110:
Warning 3: deprecated: ArgVar
Use version in [Locus]
File "src/Common/Tactics/transparent_abstract_tactics.ml", line 31, characters 34-67:
Warning 3: deprecated: ArgVar
Use version in [Locus]
CAMLOPT -c src/Common/Tactics/hint_db_extra_tactics.ml
File "src/Common/Tactics/hint_db_extra_tactics.ml", line 11, characters 58-111:
Warning 3: deprecated: ArgVar
Use version in [Locus]
File "src/Common/Tactics/hint_db_extra_tactics.ml", line 20, characters 32-65:
Warning 3: deprecated: ArgVar
Use version in [Locus]
CAMLC -c src/Common/Tactics/transparent_abstract_tactics.ml
File "src/Common/Tactics/transparent_abstract_tactics.ml", line 22, characters 57-110:
Warning 3: deprecated: ArgVar
Use version in [Locus]
File "src/Common/Tactics/transparent_abstract_tactics.ml", line 31, characters 34-67:
Warning 3: deprecated: ArgVar
Use version in [Locus]
Please make fiat-parsers compile with -w "+compatibility-notation"
Please make your project compile with -w "+compatibility-notation" to prepare for the Coq 8.9 release (at least the fiat-parsers part that we test in Coq CI). We would appreciate if this could be done ASAP. If you have trouble doing so, please raise your concern at coq/coq#8383.
[warnings] Please fix OCaml warnings
Dear devs,
in Coq we are considering requiring plugins in the CI to use the same set of compiler flags for warnings than the main Coq tree (c.f. coq/coq#9605 ), in particular, this means that the plugins should now compile warning-free, except for deprecation notices.
Note that some of the raised warnings are really fatal, [like missing match cases].
Please, try to fix OCaml warnings present in your codebase, thanks!
[coq] Please update the repository for Coq 8.12
c.f. coq/coq#11158
I tried to do it but found some problems.
On the long term it'd be great if we could avoid manual action, for example Compcert does work with unknown Coq versions but emits a warning.
nonempty git diff after coq ci build
?? compatibility/Coq__8_20__Compat.v
in _build_ci/fiat_parsers/etc/coq-scripts
coq-scripts submodule not up to date with VDFILE
I have no idea how this passed CI.
Port Fiat to coqpp
The Fiat repository should be ported to the coqpp tool for Coq master, by turning the ml4 files into mlg and adapting the code correspondingly. While the code adaptation is trivial, Fiat seems to do black magic in its makefile to pick the right file depending on the Coq version. I don't really understand that part enough to fix it though, hence this bug report.
Regarding the port, the following diff should be enough:
--- a/src/Common/Tactics/hint_db_extra_plugin.ml4.master
+++ b/src/Common/Tactics/hint_db_extra_plugin.mlg.master
@@ -1,16 +1,20 @@
+{
+
open Hint_db_extra_tactics
open Stdarg
open Ltac_plugin
open Tacarg
+}
+
DECLARE PLUGIN "hint_db_extra_plugin"
TACTIC EXTEND foreach_db
| [ "foreach" "[" ne_preident_list(l) "]" "run" tactic(k) ] ->
- [ WITH_DB.with_hint_db l k ]
+ { WITH_DB.with_hint_db l k }
END
TACTIC EXTEND addto_db
| [ "add" constr(name) "to" ne_preident_list(l) ] ->
- [ WITH_DB.add_resolve_to_db (Hints.IsConstr (name, Univ.ContextSet.empty)) l]
- END;;
+ { WITH_DB.add_resolve_to_db (Hints.IsConstr (name, Univ.ContextSet.empty)) l }
+ END--- a/src/Common/Tactics/transparent_abstract_plugin.ml4.master
+++ b/src/Common/Tactics/transparent_abstract_plugin.mlg.master
@@ -1,21 +1,25 @@
+{
+
open Transparent_abstract_tactics
open Stdarg
open Ltac_plugin
open Tacarg
+}
+
DECLARE PLUGIN "transparent_abstract_plugin"
TACTIC EXTEND transparentabstract
| [ "cache" tactic(tac) "as" ident(name)]
--> [ TRANSPARENT_ABSTRACT.tclTRABSTRACT (Some name) (Tacinterp.tactic_of_value ist tac) ]
+-> { TRANSPARENT_ABSTRACT.tclTRABSTRACT (Some name) (Tacinterp.tactic_of_value ist tac) }
END
TACTIC EXTEND abstracttermas
| [ "cache_term" constr(term) "as" ident(name) "run" tactic(tacK)] ->
-[ TRANSPARENT_ABSTRACT.tclABSTRACTTERM (Some name) term tacK ]
+{ TRANSPARENT_ABSTRACT.tclABSTRACTTERM (Some name) term tacK }
END
TACTIC EXTEND abstractterm
| [ "cache_term" constr(term) "run" tactic(tacK) ] ->
-[ TRANSPARENT_ABSTRACT.tclABSTRACTTERM None term tacK ]
-END;;
+{ TRANSPARENT_ABSTRACT.tclABSTRACTTERM None term tacK }
+ENDijcar2020 branch fails to build
Steps to reproduce:
- Create environment for ancient Coq and ancient OCaml with
opam switch create coq8.4pl6 4.02.3 - Use new environment with
eval $(opam env) - Pin ancient Coq with
opam pin add coq 8.4.6~camlp4 - Clone repo with
git clone [email protected]:mit-plv/fiat.git && mv fiat ijcar2020 cd ijcar2020git checkout ijcar2020- Follow steps in
README.rstexport COQPATH=/home/psnively/ijcar2020/bedrockmake -C bedrock -j4 facade qsfacade
Result:
make: Entering directory '/home/psnively/ijcar2020/bedrock'
make: *** No rule to make target 'Bedrock/reification/extlib.cmi', needed by 'reification'. Stop.
make: Leaving directory '/home/psnively/ijcar2020/bedrock'
I've tried examining the build system to see if I could correct the issue myself, and given up. I'm very interested in this work, but I have to say I'm extremely concerned about its being so terribly out-of-date with respect to Coq's evolution, its dependence on "vendored" third-party OCaml libraries such as extlib, its lack of integration with OPAM, and its highly magical and therefore version-dependent "wiring together" of Coq and OCaml code by means of Lovecraftian approaches to software engineering. There Has Got To Be A Better Way™, and I strongly urge your team to find it.
Current version does not build with 8.4pl6 or 8.5pl2
I'm trying to package this for Nix.
Build output from 8.4pl6:
File "/private/var/folders/c1/49wv07ys16jbhh4ry92dc8jm0000gn/T/nix-build-coq-fiat-8.4-20160929.drv-0/fiat-d0962ac/src/QueryStructure/Implementation/Operations/General/QueryRefinements.v", line 799, characters 4-15:
Error: Impossible to unify "ret (r a :: map r l)%list" with
"x0 <- (Return (r a))%QuerySpec;
ret (x0 ++ map r l)%list".
Build output from 8.5pl2:
File "./src/Computation/FixComp.v", line 574, characters 39-52:
Error:
In environment
fDom : list Type
fCod : Type
fDef : funType fDom fCod -> funType fDom fCod
fDef_monotone : forall rec rec' : funType fDom fCod,
refineFun rec rec' -> refineFun (fDef rec) (fDef rec')
The term "fDef_monotone" has type
"forall rec rec' : funType fDom fCod,
refineFun rec rec' -> refineFun (fDef rec) (fDef rec')"
while it is expected to have type "monotonic_function fDef".
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.