Skip to content

[numeral] [plugins] Remove Coq's Bigint module in favor of ZArith. #11742

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
coqbot-app merged 5 commits into from
Aug 28, 2020
Merged

[numeral] [plugins] Remove Coq's Bigint module in favor of ZArith. #11742

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
094e464
[numeral] [plugins] Switch from `Big_int` to ZArith.
ejgallego Oct 16, 2018
3fcd90f
[zarith] [notation] Build less intermediate values
ejgallego Mar 4, 2020
694afd3
[numtok] [zarith] Simplifications
ejgallego Jun 19, 2020
5a28133
[nsatz] num → zarith
vbgl Oct 16, 2018
21dd85b
[zarith] Changelog
ejgallego Jun 19, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions .gitlab-ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ stages:
variables:
# Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
# for reference]
CACHEKEY: "bionic_coq-V2020-08-18-V29"
CACHEKEY: "bionic_coq-V2020-08-28-V92"
IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
# By default, jobs run in the base switch; override to select another switch
OPAM_SWITCH: "base"
Expand Down Expand Up @@ -600,7 +600,7 @@ test-suite:edge:dune:dev:
- opam repo add ocaml-beta https://github.com/ocaml/ocaml-beta-repository.git
- opam update
- opam install ocaml-variants=$OCAMLVER
- opam install dune num
- opam install dune num zarith
- eval $(opam env)
- export COQ_UNIT_TEST=noop
- make -f Makefile.dune test-suite
Expand Down
2 changes: 2 additions & 0 deletions INSTALL.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,8 @@ To compile Coq yourself, you need:
- The [num](https://github.com/ocaml/num) library; note that it is
included in the OCaml distribution for OCaml versions < 4.06.0

- The [ZArith library](https://github.com/ocaml/Zarith) >= 1.8
Copy link
Copy Markdown
Contributor

@RalfJung RalfJung Aug 29, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The version given here is inconsistent with what it says in the opam file (1.9.1).


- The [findlib](http://projects.camlcity.org/projects/findlib.html) library (version >= 1.8.0)

- GNU Make (version >= 3.81)
Expand Down
6 changes: 3 additions & 3 deletions META.coq.in
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -120,7 +120,7 @@ package "interp" (
description = "Coq Term Interpretation"
version = "8.13"

requires = "coq.pretyping"
requires = "zarith, coq.pretyping"
directory = "interp"

archive(byte) = "interp.cma"
Expand Down Expand Up @@ -327,7 +327,7 @@ package "plugins" (
description = "Coq micromega plugin"
version = "8.13"

requires = "num,coq.plugins.ltac"
requires = "num, coq.plugins.ltac"
directory = "micromega"

archive(byte) = "micromega_plugin.cmo"
Expand Down Expand Up @@ -462,7 +462,7 @@ package "plugins" (
description = "Coq nsatz plugin"
version = "8.13"

requires = "num,coq.plugins.ltac"
requires = "zarith, coq.plugins.ltac"
directory = "nsatz"

archive(byte) = "nsatz_plugin.cmo"
Expand Down
16 changes: 2 additions & 14 deletions Makefile.build
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -245,7 +245,7 @@ COQOPTS=$(NATIVECOMPUTE) $(COQWARNERROR) $(COQUSERFLAGS)
BOOTCOQC=$(TIMER) $(COQC) -coqlib . -q $(COQOPTS)

LOCALINCLUDES=$(addprefix -I ,$(SRCDIRS))
MLINCLUDES=$(LOCALINCLUDES)
MLINCLUDES=$(LOCALINCLUDES) -package zarith

USERCONTRIBINCLUDES=$(addprefix -I user-contrib/,$(USERCONTRIBDIRS))

Expand Down Expand Up @@ -302,7 +302,7 @@ $(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ -linkpkg $(1) $^
endef

# Main packages linked by Coq.
SYSMOD:=-package num,str,unix,dynlink,threads
SYSMOD:=-package str,unix,dynlink,threads,num,zarith

###########################################################################
# Infrastructure for the rest of the Makefile
Expand Down Expand Up @@ -709,10 +709,6 @@ plugins/micromega/%.cmi: plugins/micromega/%.mli
$(SHOW)'OCAMLC $<'
$(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $<

plugins/nsatz/%.cmi: plugins/nsatz/%.mli
$(SHOW)'OCAMLC $<'
$(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $<

%.cmi: %.mli
$(SHOW)'OCAMLC $<'
$(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $<
Expand All @@ -721,10 +717,6 @@ plugins/micromega/%.cmo: plugins/micromega/%.ml
$(SHOW)'OCAMLC $<'
$(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $<

plugins/nsatz/%.cmo: plugins/nsatz/%.ml
$(SHOW)'OCAMLC $<'
$(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $<

%.cmo: %.ml
$(SHOW)'OCAMLC $<'
$(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $<
Expand Down Expand Up @@ -762,10 +754,6 @@ plugins/micromega/%.cmx: plugins/micromega/%.ml
$(SHOW)'OCAMLOPT $<'
$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -package unix,num -c $<
Comment thread
ejgallego marked this conversation as resolved.

plugins/nsatz/%.cmx: plugins/nsatz/%.ml
$(SHOW)'OCAMLOPT $<'
$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -package unix,num -c $<

plugins/%.cmx: plugins/%.ml
$(SHOW)'OCAMLOPT $<'
$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -c $<
Expand Down
6 changes: 3 additions & 3 deletions azure-pipelines.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ jobs:
powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/setup-x86_64.exe', 'setup-x86_64.exe')"
SET CYGROOT=C:\cygwin64
SET CYGCACHE=%CYGROOT%\var\cache\setup
setup-x86_64.exe -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time -P wget -P curl -P git -P mingw64-x86_64-binutils,mingw64-x86_64-gcc-core,mingw64-x86_64-gcc-g++,mingw64-x86_64-pkg-config,mingw64-x86_64-windows_default_manifest -P mingw64-x86_64-headers,mingw64-x86_64-runtime,mingw64-x86_64-pthreads,mingw64-x86_64-zlib -P python3
setup-x86_64.exe -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time -P wget -P curl -P git -P mingw64-x86_64-binutils,mingw64-x86_64-gcc-core,mingw64-x86_64-gcc-g++,mingw64-x86_64-pkg-config,mingw64-x86_64-windows_default_manifest -P mingw64-x86_64-headers,mingw64-x86_64-runtime,mingw64-x86_64-pthreads,mingw64-x86_64-zlib,mingw64-x86_64-gmp -P python3

SET TARGET_ARCH=x86_64-w64-mingw32
SET CD_MFMT=%cd:\=/%
Expand Down Expand Up @@ -64,7 +64,7 @@ jobs:
set -e
brew update
(cd $(brew --repository)/Library/Taps/homebrew/homebrew-core/ && git fetch --shallow-since=${HBCORE_DATE} && git checkout ${HBCORE_REF})
brew install gnu-time opam pkg-config gtksourceview3 adwaita-icon-theme || true
brew install gnu-time opam pkg-config gtksourceview3 adwaita-icon-theme gmp || true
# || true: workaround #12657, see also #12672 and commit message for this line
pip3 install macpack
displayName: 'Install system dependencies'
Expand All @@ -80,7 +80,7 @@ jobs:
opam switch set ocaml-base-compiler.$COMPILER
eval $(opam env)
opam update
opam install -j "$NJOBS" num ocamlfind${FINDLIB_VER} ounit lablgtk3-sourceview3
opam install -j "$NJOBS" num ocamlfind${FINDLIB_VER} ounit lablgtk3-sourceview3 zarith.1.9.1
opam list
displayName: 'Install OCaml dependencies'
env:
Expand Down
Loading