Skip to content
Snippets Groups Projects
Commit 1a9bc511 authored by Shachar Itzhaky's avatar Shachar Itzhaky
Browse files

[docs] SDK demo cosmetics.

Made the example a little bit smaller by removing some unneeded
boilerplate.
(Possible thanks to Dune 3's `glob_files_rec`.)

Also, the example now showcases `group-theory` instead of Coqoban.
Mainly because we already have Coqoban as an addon.
parent 7a97dae5
Branches
No related tags found
No related merge requests found
_build
nahas_tutorial.html
# This is quite meaningless for examples
package-lock.json
\ No newline at end of file
workdir
\ No newline at end of file
REPO = https://github.com/coq-community/coqoban
REPO = https://github.com/coq-contribs/group-theory.git
WORKDIR = workdir
PATH := $(PWD)/bin:$(PATH)
export PATH
build: $(WORKDIR)
cp dune-files/dune $(WORKDIR)/
# Use current workspace, not jsCoq's
dune build --root .
......
......@@ -2,9 +2,9 @@
(rule
(targets coq-pkgs)
(deps
(package coq-coqoban))
(glob_files_rec "*.vo"))
(action
(run npx %{env:pkgtool=jscoq} build workdir --top Coqoban
--package coq-pkgs/coqoban.coq-pkg)))
(run npx %{env:pkgtool=jscoq} build workdir --top GroupTheory
--package coq-pkgs/group-theory.coq-pkg)))
(dirs workdir)
; Copied to `workdir/` by Makefile
(coq.theory
(name GroupTheory)
(synopsis "Elements of Group Theory")
(flags -w -deprecated -w -non-full-mutual -w -local-declaration))
(include_subdirs qualified)
\ No newline at end of file
(lang dune 2.5)
(lang dune 3.1)
(using coq 0.2)
(lang dune 2.4)
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment