Skip to content
Snippets Groups Projects
Unverified Commit a426c150 authored by Emilio Jesus Gallego Arias's avatar Emilio Jesus Gallego Arias
Browse files

[addons] Support for QuickChick

Closes #137
parent 57f99a4f
No related branches found
No related tags found
No related merge requests found
......@@ -54,7 +54,8 @@ export COQBUILDDIR_REL
export ADDONS_PATH
export COQPKGS_ROOT
ADDONS = mathcomp # elpi equations dsp # iris
# Addons supported in jsCoq 0.11
ADDONS = mathcomp # extlib simpleio quickchick elpi equations dsp
all:
@echo "Welcome to jsCoq makefile. Targets are:"
......
......
# -*- mode: makefile -*-
# jscoq addon: equations
# From addons
include coq-addons/common.mk
EXTLIB_GIT=https://github.com/coq-community/coq-ext-lib
EXTLIB_HOME=$(ADDONS_PATH)/extlib
EXTLIB_DEST=coq-pkgs/ExtLib
EXTLIB_BRANCH=master
export COQBIN=$(COQDIR)/bin/
.PHONY: nothing get build jscoq-install
nothing:
# Hack, remove dune build support fow now
get:
[ -d $(EXTLIB_HOME) ] || git clone -b $(EXTLIB_BRANCH) --depth=1 $(EXTLIB_GIT) $(EXTLIB_HOME)
rm -f $(EXTLIB_HOME)/src/dune
build:
export PATH=$(COQDIR)/bin:$$PATH; cd $(EXTLIB_HOME); make && make install
jscoq-install:
mkdir -p $(EXTLIB_DEST)
$(SYNCVO) $(EXTLIB_HOME)/theories/ $(EXTLIB_DEST)
......@@ -21,7 +21,7 @@ get: $(MATHCOMP_HOME)
@true
build:
export PATH=$(COQDIR)/bin:$$PATH; cd $(MATHCOMP_HOME)/mathcomp; $(MAKE) -j $(NJOBS); $(MAKE) install
export PATH=$(COQDIR)/bin:$$PATH; cd $(MATHCOMP_HOME)/mathcomp/ssreflect; $(MAKE) -j $(NJOBS); $(MAKE) install
jscoq-install:
$(SYNCVO) $(MATHCOMP_HOME)/mathcomp/ $(COQPKGS_ROOT)/mathcomp/
......
......
# -*- mode: makefile -*-
# jscoq addon: equations
# From addons
include coq-addons/common.mk
QUICKCHICK_GIT=https://github.com/QuickChick/QuickChick.git
QUICKCHICK_HOME=$(ADDONS_PATH)/quickchick
QUICKCHICK_DEST=coq-pkgs/QuickChick
QUICKCHICK_BRANCH=8.11
export COQBIN=$(COQDIR)/bin/
.PHONY: nothing get build jscoq-install
nothing:
# Hack, remove dune build support fow now
get:
[ -d $(QUICKCHICK_HOME) ] || git clone -b $(QUICKCHICK_BRANCH) --depth=1 $(QUICKCHICK_GIT) $(QUICKCHICK_HOME)
rm -f $(QUICKCHICK_HOME)/src/dune
build:
export PATH=$(COQDIR)/bin:$$PATH; cd $(QUICKCHICK_HOME); make Makefile.coq && make -f Makefile.coq byte && make install
jscoq-install:
mkdir -p $(QUICKCHICK_DEST)
$(SYNC) $(QUICKCHICK_HOME)/src/quickchick_plugin.cma $(QUICKCHICK_DEST)
$(SYNCVO) $(QUICKCHICK_HOME)/src/ $(QUICKCHICK_DEST)
# -*- mode: makefile -*-
# jscoq addon: equations
# From addons
include coq-addons/common.mk
SIMPLEIO_GIT=https://github.com/Lysxia/coq-simple-io
SIMPLEIO_HOME=$(ADDONS_PATH)/simpleio
SIMPLEIO_DEST=coq-pkgs/SimpleIO
SIMPLEIO_BRANCH=master
export COQBIN=$(COQDIR)/bin/
.PHONY: nothing get build jscoq-install
nothing:
# Hack, remove dune build support fow now
get:
[ -d $(SIMPLEIO_HOME) ] || git clone -b $(SIMPLEIO_BRANCH) --depth=1 $(SIMPLEIO_GIT) $(SIMPLEIO_HOME)
rm -f $(SIMPLEIO_HOME)/src/dune
build:
export PATH=$(COQDIR)/bin:$$PATH; cd $(SIMPLEIO_HOME); make && make install
jscoq-install:
mkdir -p $(SIMPLEIO_DEST)
$(SYNCVO) $(SIMPLEIO_HOME)/src/ $(SIMPLEIO_DEST)
......@@ -365,4 +365,10 @@ let pkgs : (string * string list * (string list * selector) list) list =
; [ "Equations" ; "Prop" ]
]
; "simpleio", [ "extlib" ], all_of
[ [ "SimpleIO" ] ]
; "quickchick", [ "coq-reals"; "extlib" ; "simpleio" ], all_of
[ [ "QuickChick" ]
]
]
......@@ -231,7 +231,7 @@ Qed.</textarea>
base_path: './',
editor: { mode: { 'company-coq': true }, keyMap: 'default' },
init_pkgs: ['init'],
all_pkgs: ['init', 'coq-base', 'coq-collections', 'coq-arith', 'coq-reals', 'mathcomp', 'equations', 'elpi', 'lf', 'plf']
all_pkgs: ['init', 'coq-base', 'coq-collections', 'coq-arith', 'coq-reals', 'mathcomp', 'equations', 'elpi', 'quickchick', 'lf', 'plf']
};
/* Global reference */
......
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please to comment