diff options
31 files changed, 346 insertions, 182 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 3c427793e2..3c24ec28c4 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -47,9 +47,6 @@ before_script: - opam list - opam config list -after_script: - - echo "The build completed normally (not a runner failure)." - ################ GITLAB CACHING ###################### # - use artifacts between jobs # ###################################################### @@ -662,5 +659,5 @@ plugin:plugin-tutorial: plugin:ci-quickchick: extends: .ci-template-flambda -plugin:ci-relation-algebra: +plugin:ci-relation_algebra: extends: .ci-template diff --git a/CHANGES.md b/CHANGES.md index fc7272da65..9a292562ed 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -22,6 +22,9 @@ Coqide - CoqIDE now properly sets the module name for a given file based on its path, see -topfile change entry for more details. +- Preferences from coqide.keys are no longer overridden by modifiers + preferences in coqiderc. + Coqtop - the use of `coqtop` as a compiler has been deprecated, in favor of diff --git a/META.coq.in b/META.coq.in index ab142ccc43..ef5de8da2b 100644 --- a/META.coq.in +++ b/META.coq.in @@ -315,7 +315,7 @@ package "plugins" ( archive(native) = "micromega_plugin.cmx" ) - package "newring" ( + package "setoid_ring" ( description = "Coq newring plugin" version = "8.10" @@ -351,7 +351,7 @@ package "plugins" ( archive(native) = "cc_plugin.cmx" ) - package "ground" ( + package "firstorder" ( description = "Coq ground plugin" version = "8.10" @@ -387,7 +387,7 @@ package "plugins" ( archive(native) = "btauto_plugin.cmx" ) - package "recdef" ( + package "funind" ( description = "Coq recdef plugin" version = "8.10" diff --git a/Makefile.ci b/Makefile.ci index 000725b6b1..a244c17ef3 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -38,7 +38,7 @@ CI_TARGETS= \ ci-mtac2 \ ci-paramcoq \ ci-quickchick \ - ci-relation-algebra \ + ci-relation_algebra \ ci-sf \ ci-simple-io \ ci-stdlib2 \ diff --git a/Makefile.doc b/Makefile.doc index e89a20393c..23aa66a1b8 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -31,8 +31,8 @@ DVIPS:=dvips HTMLSTYLE:=coqremote # Sphinx-related variables -OSNAME:=$(shell uname -o) -ifeq ($(OSNAME),Cygwin) +OSNAME:=$(shell uname -s) +ifeq ($(findstring CYGWIN,$(OSNAME)),CYGWIN) WIN_CURDIR:=$(shell cygpath -w $(CURDIR)) SPHINXENV:=COQBIN="$(CURDIR)/bin/" COQLIB="$(WIN_CURDIR)" else diff --git a/Makefile.ide b/Makefile.ide index 8f9088a04a..4cec7aa443 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -68,6 +68,7 @@ GTKBIN=$(shell pkg-config --variable=prefix gtk+-3.0)/bin GTKLIBS=$(shell pkg-config --variable=libdir gtk+-3.0) PIXBUFBIN=$(shell pkg-config --variable=prefix gdk-pixbuf-2.0)/bin SOURCEVIEWSHARE=$(shell pkg-config --variable=prefix gtksourceview-3.0)/share +ADWAITASHARE=$(shell ls -d /usr/local/Cellar/adwaita-icon-theme/*)/share ########################################################################### # CoqIde special targets @@ -255,6 +256,9 @@ $(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents $(INSTALLLIB) "$(SOURCEVIEWSHARE)/"gtksourceview-3.0/styles/{styles.rng,classic.xml} $@/gtksourceview-3.0/styles/ cp -R "$(GTKSHARE)/"locale $@ cp -R "$(GTKSHARE)/"themes $@ + $(MKDIR) $@/glib-2.0/schemas + glib-compile-schemas --targetdir=$@/glib-2.0/schemas "$(GTKSHARE)/"glib-2.0/schemas/ + cp -R "$(ADWAITASHARE)/"icons $@ $(COQIDEAPP)/Contents/Resources/loaders: $(COQIDEAPP)/Contents $(MKDIR) $@ diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 6fcc64f77e..f09087b172 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -52,7 +52,7 @@ jobs: - script: | set -e brew update - brew install gnu-time opam pkg-config gtksourceview3 + brew install gnu-time opam pkg-config gtksourceview3 adwaita-icon-theme pip3 install macpack displayName: 'Install system dependencies' diff --git a/coq-refman.opam b/coq-refman.opam index b9500243a3..16be422c27 100644 --- a/coq-refman.opam +++ b/coq-refman.opam @@ -17,7 +17,7 @@ license: "Open Publication License" depends: [ "dune" { build } - "coq" { build } + "coq" { build & = version } ] build-env: [ @@ -20,7 +20,7 @@ license: "LGPL-2.1" depends: [ "ocaml" { >= "4.05.0" } - "dune" { build & >= "1.4.0" } + "dune" { build & >= "1.6.0" } "ocamlfind" { build } "num" ] diff --git a/coqide-server.opam b/coqide-server.opam index ed6f3d98d8..0325d2549c 100644 --- a/coqide-server.opam +++ b/coqide-server.opam @@ -19,8 +19,8 @@ dev-repo: "git+https://github.com/coq/coq.git" license: "LGPL-2.1" depends: [ - "dune" { build & >= "1.4.0" } - "coq" + "dune" { build & >= "1.6.0" } + "coq" { = version } ] build: [ [ "dune" "build" "-p" name "-j" jobs ] ] diff --git a/coqide.opam b/coqide.opam index c82fa72564..2507acbb26 100644 --- a/coqide.opam +++ b/coqide.opam @@ -17,8 +17,8 @@ dev-repo: "git+https://github.com/coq/coq.git" license: "LGPL-2.1" depends: [ - "dune" { build & >= "1.4.0" } - "coqide-server" + "dune" { build & >= "1.6.0" } + "coqide-server" { = version } "lablgtk3" { >= "3.0.beta5" } "lablgtk3-sourceview3" { >= "3.0.beta5" } ] diff --git a/dev/ci/README-users.md b/dev/ci/README-users.md index 01769aeddb..06b617d4c1 100644 --- a/dev/ci/README-users.md +++ b/dev/ci/README-users.md @@ -45,6 +45,26 @@ using [coqbot](https://github.com/coq/bot); meanwhile, a workaround is to give merge permissions to someone from the Coq team as to help with these kind of merges. +### OCaml and plugin-specific considerations + +Developments that link against Coq's OCaml API [most of them are known +as "plugins"] do have some special requirements: + +- Coq's OCaml API is not stable. We hope to improve this in the future + but as of today you should expect to have to merge a fair amount of + "overlays", usually in the form of Pull Requests from Coq developers + in order to keep your plugin compatible with Coq master. + + In order to alleviate the load, you can delegate the merging of such + compatibility pull requests to Coq developers themselves, by + granting access to the plugin repository or by using `bots` such as + [Bors](https://github.com/apps/bors) that allow for automatic + management of Pull Requests. + +- Plugins in the CI should compile with the OCaml flags that Coq + uses. In particular, warnings that are considered fatal by the Coq + developers _must_ be also fatal for plugin CI code. + ### Add your development by submitting a pull request Add a new `ci-mydev.sh` script to [`dev/ci`](.); set the corresponding diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 0c89809ee9..4f5988c59c 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -254,7 +254,7 @@ : "${paramcoq_CI_ARCHIVEURL:=${paramcoq_CI_GITURL}/archive}" ######################################################################## -# relation-algebra +# relation_algebra ######################################################################## : "${relation_algebra_CI_REF:=master}" : "${relation_algebra_CI_GITURL:=https://github.com/damien-pous/relation-algebra}" diff --git a/dev/ci/ci-relation-algebra.sh b/dev/ci/ci-relation_algebra.sh index 84bed5bdfe..84bed5bdfe 100755 --- a/dev/ci/ci-relation-algebra.sh +++ b/dev/ci/ci-relation_algebra.sh diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 40c3c32e4f..4533a4dc01 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -20,6 +20,15 @@ General deprecation removed. Please, make sure your plugin is warning-free in 8.8 before trying to port it over 8.9. +Warnings + +- Coq now builds plugins with `-warn-error` enabled by default. The + amount of dangerous warnings in plugin code was very high, so we now + require plugins in the CI to adhere to the Coq warning policy. We + _strongly_ recommend against disabling the default set of warnings. + If you have special needs, see the documentation of your build + system and/or OCaml for further help. + Names - Kernel names no longer contain a section path. They now have only two diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index f532e1b68f..01c2b574a2 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -195,6 +195,18 @@ Conversion machines GH issue number: ? risk: + component: "virtual machine" (compilation to bytecode ran by a C-interpreter) + summary: primitive integer emulation layer on 32 bits not robust to garbage collection + introduced: master (before v8.10 in GH pull request #6914) + impacted released versions: none + impacted development branches: + impacted coqchk versions: none (no virtual machine in coqchk) + fixed in: + found by: Roux, Melquiond + exploit: + GH issue number: #9925 + risk: + component: "native" conversion machine (translation to OCaml which compiles to native code) summary: translation of identifier from Coq to OCaml was not bijective, leading to identify True and False introduced: V8.5 diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index b069cf27f4..a5e9023732 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -433,22 +433,26 @@ few other commands related to typeclasses. .. _TypeclassesTransparent: -Typeclasses Transparent, Typclasses Opaque -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Typeclasses Transparent, Typeclasses Opaque +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. cmd:: Typeclasses Transparent {+ @ident} This command makes the identifiers transparent during typeclass resolution. + Shortcut for :n:`Hint Transparent {+ @ident } : typeclass_instances`. .. cmd:: Typeclasses Opaque {+ @ident} - Make the identifiers opaque for typeclass search. It is useful when some - constants prevent some unifications and make resolution fail. It is also - useful to declare constants which should never be unfolded during - proof-search, like fixpoints or anything which does not look like an - abbreviation. This can additionally speed up proof search as the typeclass - map can be indexed by such rigid constants (see + Make the identifiers opaque for typeclass search. + Shortcut for :n:`Hint Opaque {+ @ident } : typeclass_instances`. + + It is useful when some constants prevent some unifications and make + resolution fail. It is also useful to declare constants which + should never be unfolded during proof-search, like fixpoints or + anything which does not look like an abbreviation. This can + additionally speed up proof search as the typeclass map can be + indexed by such rigid constants (see :ref:`thehintsdatabasesforautoandeauto`). By default, all constants and local variables are considered transparent. One @@ -458,8 +462,6 @@ type, like: .. coqdoc:: Definition relation A := A -> A -> Prop. -This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``. - Settings ~~~~~~~~ diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 8346b72cb9..35231610fe 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -144,6 +144,10 @@ Here we describe only few of them. :CAMLFLAGS: can be used to specify additional flags to the |OCaml| compiler, like ``-bin-annot`` or ``-w``.... +:OCAMLWARN: + it contains a default of ``-warn-error +a-3``, useful to modify + this setting; beware this is not recommended for projects in + Coq's CI. :COQC, COQDEP, COQDOC: can be set in order to use alternative binaries (e.g. wrappers) diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index e6922408aa..8d9e99b9d5 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -4724,6 +4724,12 @@ Non-logical tactics from the shelf into focus, by appending them to the end of the current list of focused goals. +.. tacn:: unshelve @tactic + :name: unshelve + + Performs :n:`@tactic`, then unshelves existential variables added to the + shelf by the execution of :n:`@tactic`, prepending them to the current goal. + .. tacn:: give_up :name: give_up diff --git a/ide/.merlin.in b/ide/.merlin.in index 4dc6f45550..b8d7953833 100644 --- a/ide/.merlin.in +++ b/ide/.merlin.in @@ -1,4 +1,4 @@ -PKG unix laglgtk2 lablgtk2.sourceview2 +PKG unix laglgtk3 lablgtk3-sourceview3 S utils B utils diff --git a/ide/preferences.ml b/ide/preferences.ml index 47cd4c58b6..3893d023bd 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -263,8 +263,6 @@ let get_unicode_bindings_default_file () = (** Hooks *) -(** New style preferences *) - let cmd_coqtop = new preference ~name:["cmd_coqtop"] ~init:None ~repr:Repr.(option string) @@ -645,8 +643,6 @@ let tag_button () = let box = GPack.hbox () in new tag_button (Gobject.unsafe_cast box#as_widget) -(** Old style preferences *) - let save_pref () = if not (Sys.file_exists (Minilib.coqide_config_home ())) then Unix.mkdir (Minilib.coqide_config_home ()) 0o700; @@ -658,15 +654,18 @@ let save_pref () = Config_lexer.print_file pref_file prefs let load_pref () = + (* Load main preference file *) + let () = + let m = Config_lexer.load_file loaded_pref_file in + let iter name v = + if Util.String.Map.mem name !preferences then + try (Util.String.Map.find name !preferences).set v with _ -> () + else unknown_preferences := Util.String.Map.add name v !unknown_preferences + in + Util.String.Map.iter iter m in + (* Load file for bindings *) let () = try GtkData.AccelMap.load loaded_accel_file with _ -> () in - - let m = Config_lexer.load_file loaded_pref_file in - let iter name v = - if Util.String.Map.mem name !preferences then - try (Util.String.Map.find name !preferences).set v with _ -> () - else unknown_preferences := Util.String.Map.add name v !unknown_preferences - in - Util.String.Map.iter iter m + () let pstring name p = string ~f:p#set name p#get let pbool name p = bool ~f:p#set name p#get diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index d2c88bffcc..2293ae9dfd 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -193,6 +193,12 @@ if (sp - num_args < coq_stack_threshold) { \ #define AllocCarry(cond) Alloc_small(accu, 1, (cond)? coq_tag_C1 : coq_tag_C0) #define AllocPair() Alloc_small(accu, 2, coq_tag_pair) +#define Swap_accu_sp do{ \ + value swap_accu_sp_tmp__ = accu; \ + accu = *sp; \ + *sp = swap_accu_sp_tmp__; \ + }while(0) + /* For signal handling, we hijack some code from the caml runtime */ extern intnat caml_signals_are_pending; @@ -1213,7 +1219,7 @@ value coq_interprete /* Adds the integer in the accumulator with the one ontop of the stack (which is poped)*/ print_instr("ADDINT63"); - accu = uint63_add(accu, *sp++); + Uint63_add(accu, *sp++); Next; } @@ -1221,10 +1227,12 @@ value coq_interprete print_instr("CHECKADDCINT63"); CheckInt2(); /* returns the sum with a carry */ - value s; - s = uint63_add(accu, *sp++); - AllocCarry(uint63_lt(s,accu)); - Field(accu, 0) = s; + int c; + Uint63_add(accu, *sp); + Uint63_lt(c, accu, *sp); + Swap_accu_sp; + AllocCarry(c); + Field(accu, 0) = *sp++; Next; } @@ -1232,10 +1240,12 @@ value coq_interprete print_instr("ADDCARRYCINT63"); CheckInt2(); /* returns the sum plus one with a carry */ - value s; - s = uint63_addcarry(accu, *sp++); - AllocCarry(uint63_leq(s, accu)); - Field(accu, 0) = s; + int c; + Uint63_addcarry(accu, *sp); + Uint63_leq(c, accu, *sp); + Swap_accu_sp; + AllocCarry(c); + Field(accu, 0) = *sp++; Next; } @@ -1246,7 +1256,7 @@ value coq_interprete Instruct (SUBINT63) { print_instr("SUBINT63"); /* returns the subtraction */ - accu = uint63_sub(accu, *sp++); + Uint63_sub(accu, *sp++); Next; } @@ -1254,12 +1264,12 @@ value coq_interprete print_instr("SUBCINT63"); CheckInt2(); /* returns the subtraction with a carry */ - value b; - value s; - b = *sp++; - s = uint63_sub(accu,b); - AllocCarry(uint63_lt(accu,b)); - Field(accu, 0) = s; + int c; + Uint63_lt(c, accu, *sp); + Uint63_sub(accu, *sp); + Swap_accu_sp; + AllocCarry(c); + Field(accu, 0) = *sp++; Next; } @@ -1267,12 +1277,12 @@ value coq_interprete print_instr("SUBCARRYCINT63"); CheckInt2(); /* returns the subtraction minus one with a carry */ - value b; - value s; - b = *sp++; - s = uint63_subcarry(accu,b); - AllocCarry(uint63_leq(accu,b)); - Field(accu, 0) = s; + int c; + Uint63_leq(c,accu,*sp); + Uint63_subcarry(accu,*sp); + Swap_accu_sp; + AllocCarry(c); + Field(accu, 0) = *sp++; Next; } @@ -1280,7 +1290,7 @@ value coq_interprete print_instr("MULINT63"); CheckInt2(); /* returns the multiplication */ - accu = uint63_mul(accu,*sp++); + Uint63_mul(accu,*sp++); Next; } @@ -1294,9 +1304,11 @@ value coq_interprete AllocPair(); */ /* Field(accu, 0) = (value)(I64_lsr(p,31)|1) ; */ /*higher part*/ /* Field(accu, 1) = (value)(I64_to_int32(p)|1); */ /*lower part*/ - value x = accu; + Uint63_mulc(accu, *sp, sp); + *--sp = accu; AllocPair(); - Field(accu, 1) = uint63_mulc(x, *sp++, &Field(accu, 0)); + Field(accu, 1) = *sp++; + Field(accu, 0) = *sp++; Next; } @@ -1306,13 +1318,13 @@ value coq_interprete /* spiwack: a priori no need of the NON_STANDARD_DIV_MOD flag since it probably only concerns negative number. needs to be checked at this point */ - value divisor; - divisor = *sp++; - if (uint63_eq0(divisor)) { - accu = divisor; + int b; + Uint63_eq0(b, *sp); + if (b) { + accu = *sp++; } else { - accu = uint63_div(accu, divisor); + Uint63_div(accu, *sp++); } Next; } @@ -1320,13 +1332,13 @@ value coq_interprete Instruct(CHECKMODINT63) { print_instr("CHEKMODINT63"); CheckInt2(); - value divisor; - divisor = *sp++; - if (uint63_eq0(divisor)) { - accu = divisor; + int b; + Uint63_eq0(b, *sp); + if (b) { + accu = *sp++; } else { - accu = uint63_mod(accu,divisor); + Uint63_mod(accu,*sp++); } Next; } @@ -1337,19 +1349,24 @@ value coq_interprete /* spiwack: a priori no need of the NON_STANDARD_DIV_MOD flag since it probably only concerns negative number. needs to be checked at this point */ - value divisor; - divisor = *sp++; - if (uint63_eq0(divisor)) { - Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */ - Field(accu, 0) = divisor; - Field(accu, 1) = divisor; + int b; + Uint63_eq0(b, *sp); + if (b) { + AllocPair(); + Field(accu, 0) = *sp; + Field(accu, 1) = *sp++; } else { - value modulus; - modulus = accu; - Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */ - Field(accu, 0) = uint63_div(modulus,divisor); - Field(accu, 1) = uint63_mod(modulus,divisor); + *--sp = accu; + Uint63_div(sp[0],sp[1]); + Swap_accu_sp; + Uint63_mod(accu,sp[1]); + sp[1] = sp[0]; + Swap_accu_sp; + AllocPair(); + Field(accu, 0) = sp[1]; + Field(accu, 1) = sp[0]; + sp += 2; } Next; } @@ -1376,59 +1393,57 @@ value coq_interprete Field(accu, 0) = value_of_uint32(I64_to_int32(quo)); Field(accu, 1) = value_of_uint32(I64_to_int32(mod)); } */ - value bigint; /* TODO: fix */ - bigint = *sp++; /* TODO: take accu into account */ - value divisor; - divisor = *sp++; - if (uint63_eq0(divisor)) { - Alloc_small(accu, 2, 1); - Field(accu, 0) = divisor; - Field(accu, 1) = divisor; + int b; + Uint63_eq0(b, sp[1]); + if (b) { + AllocPair(); + Field(accu, 0) = sp[1]; + Field(accu, 1) = sp[1]; } else { - value quo, mod; - mod = uint63_div21(accu, bigint, divisor, &quo); - Alloc_small(accu, 2, 1); - Field(accu, 0) = quo; - Field(accu, 1) = mod; + Uint63_div21(accu, sp[0], sp[1], sp); + sp[1] = sp[0]; + Swap_accu_sp; + AllocPair(); + Field(accu, 0) = sp[1]; + Field(accu, 1) = sp[0]; } + sp += 2; Next; } Instruct(CHECKLXORINT63) { print_instr("CHECKLXORINT63"); CheckInt2(); - accu = uint63_lxor(accu,*sp++); + Uint63_lxor(accu,*sp++); Next; } Instruct(CHECKLORINT63) { print_instr("CHECKLORINT63"); CheckInt2(); - accu = uint63_lor(accu,*sp++); + Uint63_lor(accu,*sp++); Next; } Instruct(CHECKLANDINT63) { print_instr("CHECKLANDINT63"); CheckInt2(); - accu = uint63_land(accu,*sp++); + Uint63_land(accu,*sp++); Next; } Instruct(CHECKLSLINT63) { print_instr("CHECKLSLINT63"); CheckInt2(); - value p = *sp++; - accu = uint63_lsl(accu,p); + Uint63_lsl(accu,*sp++); Next; } Instruct(CHECKLSRINT63) { print_instr("CHECKLSRINT63"); CheckInt2(); - value p = *sp++; - accu = uint63_lsr(accu,p); + Uint63_lsr(accu,*sp++); Next; } @@ -1436,7 +1451,7 @@ value coq_interprete print_instr("CHECKLSLINT63CONST1"); if (Is_uint63(accu)) { pc++; - accu = uint63_lsl1(accu); + Uint63_lsl1(accu); Next; } else { *--sp = uint63_one(); @@ -1450,7 +1465,7 @@ value coq_interprete print_instr("CHECKLSRINT63CONST1"); if (Is_uint63(accu)) { pc++; - accu = uint63_lsr1(accu); + Uint63_lsr1(accu); Next; } else { *--sp = uint63_one(); @@ -1463,18 +1478,17 @@ value coq_interprete Instruct (CHECKADDMULDIVINT63) { print_instr("CHECKADDMULDIVINT63"); CheckInt3(); - value x; - value y; - x = *sp++; - y = *sp++; - accu = uint63_addmuldiv(accu,x,y); + Uint63_addmuldiv(accu,sp[0],sp[1]); + sp += 2; Next; } Instruct (CHECKEQINT63) { print_instr("CHECKEQINT63"); CheckInt2(); - accu = uint63_eq(accu,*sp++) ? coq_true : coq_false; + int b; + Uint63_eq(b, accu, *sp++); + accu = b ? coq_true : coq_false; Next; } @@ -1484,7 +1498,9 @@ value coq_interprete } Instruct (LTINT63) { print_instr("LTINT63"); - accu = uint63_lt(accu,*sp++) ? coq_true : coq_false; + int b; + Uint63_lt(b,accu,*sp++); + accu = b ? coq_true : coq_false; Next; } @@ -1494,7 +1510,9 @@ value coq_interprete } Instruct (LEINT63) { print_instr("LEINT63"); - accu = uint63_leq(accu,*sp++) ? coq_true : coq_false; + int b; + Uint63_leq(b,accu,*sp++); + accu = b ? coq_true : coq_false; Next; } @@ -1503,25 +1521,30 @@ value coq_interprete /* assumes Inductive _ : _ := Eq | Lt | Gt */ print_instr("CHECKCOMPAREINT63"); CheckInt2(); - if (uint63_eq(accu,*sp)) { + int b; + Uint63_eq(b, accu, *sp); + if (b) { accu = coq_Eq; sp++; } - else accu = uint63_lt(accu,*sp++) ? coq_Lt : coq_Gt; + else { + Uint63_lt(b, accu, *sp++); + accu = b ? coq_Lt : coq_Gt; + } Next; } Instruct (CHECKHEAD0INT63) { print_instr("CHECKHEAD0INT63"); CheckInt1(); - accu = uint63_head0(accu); + Uint63_head0(accu); Next; } Instruct (CHECKTAIL0INT63) { print_instr("CHECKTAIL0INT63"); CheckInt1(); - accu = uint63_tail0(accu); + Uint63_tail0(accu); Next; } diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h index 9375b15de2..1ea461c5e5 100644 --- a/kernel/byterun/coq_memory.h +++ b/kernel/byterun/coq_memory.h @@ -19,7 +19,7 @@ #define Coq_stack_size (4096 * sizeof(value)) -#define Coq_stack_threshold (256 * sizeof(value)) +#define Coq_stack_threshold (256 * sizeof(value)) /* see kernel/cbytegen.ml */ #define Coq_max_stack_size (256 * 1024) #define TRANSP 0 diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h index 5499f124a2..d982f67566 100644 --- a/kernel/byterun/coq_uint63_emul.h +++ b/kernel/byterun/coq_uint63_emul.h @@ -15,83 +15,142 @@ value uint63_##name() { \ } # define DECLARE_UNOP(name) \ -value uint63_##name(value x) { \ +value uint63_##name##_ml(value x) { \ static value* cb = 0; \ CAMLparam1(x); \ if (!cb) cb = caml_named_value("uint63 " #name); \ CAMLreturn(caml_callback(*cb, x)); \ } -# define DECLARE_PREDICATE(name) \ -value uint63_##name(value x) { \ - static value* cb = 0; \ - CAMLparam1(x); \ - if (!cb) cb = caml_named_value("uint63 " #name); \ - CAMLreturn(Int_val(caml_callback(*cb, x))); \ - } +# define CALL_UNOP_NOASSIGN(name, x) \ + value uint63_return_value__; \ + value uint63_arg_x__ = (x); \ + Setup_for_gc; \ + uint63_return_value__ = uint63_##name##_ml(uint63_arg_x__); \ + Restore_after_gc + +# define CALL_UNOP(name, x) do{ \ + CALL_UNOP_NOASSIGN(name, x); \ + accu = uint63_return_value__; \ + }while(0) + +# define CALL_PREDICATE(r, name, x) do{ \ + CALL_UNOP_NOASSIGN(name, x); \ + (r) = Int_val(uint63_return_value__); \ + }while(0) # define DECLARE_BINOP(name) \ -value uint63_##name(value x, value y) { \ +value uint63_##name##_ml(value x, value y) { \ static value* cb = 0; \ CAMLparam2(x, y); \ if (!cb) cb = caml_named_value("uint63 " #name); \ CAMLreturn(caml_callback2(*cb, x, y)); \ } -# define DECLARE_RELATION(name) \ -value uint63_##name(value x, value y) { \ - static value* cb = 0; \ - CAMLparam2(x, y); \ - if (!cb) cb = caml_named_value("uint63 " #name); \ - CAMLreturn(Int_val(caml_callback2(*cb, x, y))); \ - } +# define CALL_BINOP_NOASSIGN(name, x, y) \ + value uint63_return_value__; \ + value uint63_arg_x__ = (x); \ + value uint63_arg_y__ = (y); \ + Setup_for_gc; \ + uint63_return_value__ = uint63_##name##_ml(uint63_arg_x__, uint63_arg_y__); \ + Restore_after_gc + +# define CALL_BINOP(name, x, y) do{ \ + CALL_BINOP_NOASSIGN(name, x, y); \ + accu = uint63_return_value__; \ + }while(0) + +# define CALL_RELATION(r, name, x, y) do{ \ + CALL_BINOP_NOASSIGN(name, x, y); \ + (r) = Int_val(uint63_return_value__); \ + }while(0) # define DECLARE_TEROP(name) \ -value uint63_##name(value x, value y, value z) { \ +value uint63_##name##_ml(value x, value y, value z) { \ static value* cb = 0; \ CAMLparam3(x, y, z); \ if (!cb) cb = caml_named_value("uint63 " #name); \ CAMLreturn(caml_callback3(*cb, x, y, z)); \ } +# define CALL_TEROP(name, x, y, z) do{ \ + value uint63_return_value__; \ + value uint63_arg_x__ = (x); \ + value uint63_arg_y__ = (y); \ + value uint63_arg_z__ = (z); \ + Setup_for_gc; \ + uint63_return_value__ = uint63_##name##_ml(uint63_arg_x__, uint63_arg_y__, uint63_arg_z__); \ + Restore_after_gc; \ + accu = uint63_return_value__; \ + }while(0) DECLARE_NULLOP(one) DECLARE_BINOP(add) +#define Uint63_add(x, y) CALL_BINOP(add, x, y) DECLARE_BINOP(addcarry) +#define Uint63_addcarry(x, y) CALL_BINOP(addcarry, x, y) DECLARE_TEROP(addmuldiv) +#define Uint63_addmuldiv(x, y, z) CALL_TEROP(addmuldiv, x, y, z) DECLARE_BINOP(div) -DECLARE_TEROP(div21_ml) -DECLARE_RELATION(eq) -DECLARE_PREDICATE(eq0) +#define Uint63_div(x, y) CALL_BINOP(div, x, y) +DECLARE_BINOP(eq) +#define Uint63_eq(r, x, y) CALL_RELATION(r, eq, x, y) +DECLARE_UNOP(eq0) +#define Uint63_eq0(r, x) CALL_PREDICATE(r, eq0, x) DECLARE_UNOP(head0) +#define Uint63_head0(x) CALL_UNOP(head0, x) DECLARE_BINOP(land) -DECLARE_RELATION(leq) +#define Uint63_land(x, y) CALL_BINOP(land, x, y) +DECLARE_BINOP(leq) +#define Uint63_leq(r, x, y) CALL_RELATION(r, leq, x, y) DECLARE_BINOP(lor) +#define Uint63_lor(x, y) CALL_BINOP(lor, x, y) DECLARE_BINOP(lsl) +#define Uint63_lsl(x, y) CALL_BINOP(lsl, x, y) DECLARE_UNOP(lsl1) +#define Uint63_lsl1(x) CALL_UNOP(lsl1, x) DECLARE_BINOP(lsr) +#define Uint63_lsr(x, y) CALL_BINOP(lsr, x, y) DECLARE_UNOP(lsr1) -DECLARE_RELATION(lt) +#define Uint63_lsr1(x) CALL_UNOP(lsr1, x) +DECLARE_BINOP(lt) +#define Uint63_lt(r, x, y) CALL_RELATION(r, lt, x, y) DECLARE_BINOP(lxor) +#define Uint63_lxor(x, y) CALL_BINOP(lxor, x, y) DECLARE_BINOP(mod) +#define Uint63_mod(x, y) CALL_BINOP(mod, x, y) DECLARE_BINOP(mul) -DECLARE_BINOP(mulc_ml) +#define Uint63_mul(x, y) CALL_BINOP(mul, x, y) DECLARE_BINOP(sub) +#define Uint63_sub(x, y) CALL_BINOP(sub, x, y) DECLARE_BINOP(subcarry) +#define Uint63_subcarry(x, y) CALL_BINOP(subcarry, x, y) DECLARE_UNOP(tail0) +#define Uint63_tail0(x) CALL_UNOP(tail0, x) + +DECLARE_TEROP(div21_ml) +# define Uint63_div21(x, y, z, q) do{ \ + value uint63_return_value__; \ + value uint63_arg_x__ = (x); \ + value uint63_arg_y__ = (y); \ + value uint63_arg_z__ = (z); \ + Setup_for_gc; \ + uint63_return_value__ = \ + uint63_div21_ml_ml(uint63_arg_x__, uint63_arg_y__, uint63_arg_z__); \ + Restore_after_gc; \ + *q = Field(uint63_return_value__, 0); \ + accu = Field(uint63_return_value__, 1); \ + }while(0) -value uint63_div21(value x, value y, value z, value* q) { - CAMLparam3(x, y, z); - CAMLlocal1(qr); - qr = uint63_div21_ml(x, y, z); - *q = Field(qr, 0); - CAMLreturn(Field(qr, 1)); -} - -value uint63_mulc(value x, value y, value* h) { - CAMLparam2(x, y); - CAMLlocal1(hl); - hl = uint63_mulc_ml(x, y); - *h = Field(hl, 0); - CAMLreturn(Field(hl, 1)); -} +DECLARE_BINOP(mulc_ml) +# define Uint63_mulc(x, y, h) do{ \ + value uint63_return_value__; \ + value uint63_arg_x__ = (x); \ + value uint63_arg_y__ = (y); \ + Setup_for_gc; \ + uint63_return_value__ = \ + uint63_mulc_ml_ml(uint63_arg_x__, uint63_arg_y__); \ + Restore_after_gc; \ + *(h) = Field(uint63_return_value__, 0); \ + accu = Field(uint63_return_value__, 1); \ + }while(0) diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h index 92f4dc79bc..d431dc1e5c 100644 --- a/kernel/byterun/coq_uint63_native.h +++ b/kernel/byterun/coq_uint63_native.h @@ -9,28 +9,43 @@ #define uint63_one() ((value) 3) /* 2*1 + 1 */ #define uint63_eq(x,y) ((x) == (y)) -#define uint63_eq0(x) ((x) == (uint64_t)1) +#define Uint63_eq(r,x,y) ((r) = uint63_eq(x,y)) +#define Uint63_eq0(r,x) ((r) = ((x) == (uint64_t)1)) #define uint63_lt(x,y) ((uint64_t) (x) < (uint64_t) (y)) +#define Uint63_lt(r,x,y) ((r) = uint63_lt(x,y)) #define uint63_leq(x,y) ((uint64_t) (x) <= (uint64_t) (y)) +#define Uint63_leq(r,x,y) ((r) = uint63_leq(x,y)) -#define uint63_add(x,y) ((value)((uint64_t) (x) + (uint64_t) (y) - 1)) -#define uint63_addcarry(x,y) ((value)((uint64_t) (x) + (uint64_t) (y) + 1)) -#define uint63_sub(x,y) ((value)((uint64_t) (x) - (uint64_t) (y) + 1)) -#define uint63_subcarry(x,y) ((value)((uint64_t) (x) - (uint64_t) (y) - 1)) -#define uint63_mul(x,y) (Val_long(uint63_of_value(x) * uint63_of_value(y))) -#define uint63_div(x,y) (Val_long(uint63_of_value(x) / uint63_of_value(y))) -#define uint63_mod(x,y) (Val_long(uint63_of_value(x) % uint63_of_value(y))) +#define Uint63_add(x,y) (accu = (value)((uint64_t) (x) + (uint64_t) (y) - 1)) +#define Uint63_addcarry(x,y) (accu = (value)((uint64_t) (x) + (uint64_t) (y) + 1)) +#define Uint63_sub(x,y) (accu = (value)((uint64_t) (x) - (uint64_t) (y) + 1)) +#define Uint63_subcarry(x,y) (accu = (value)((uint64_t) (x) - (uint64_t) (y) - 1)) +#define Uint63_mul(x,y) (accu = Val_long(uint63_of_value(x) * uint63_of_value(y))) +#define Uint63_div(x,y) (accu = Val_long(uint63_of_value(x) / uint63_of_value(y))) +#define Uint63_mod(x,y) (accu = Val_long(uint63_of_value(x) % uint63_of_value(y))) -#define uint63_lxor(x,y) ((value)(((uint64_t)(x) ^ (uint64_t)(y)) | 1)) -#define uint63_lor(x,y) ((value)((uint64_t)(x) | (uint64_t)(y))) -#define uint63_land(x,y) ((value)((uint64_t)(x) & (uint64_t)(y))) +#define Uint63_lxor(x,y) (accu = (value)(((uint64_t)(x) ^ (uint64_t)(y)) | 1)) +#define Uint63_lor(x,y) (accu = (value)((uint64_t)(x) | (uint64_t)(y))) +#define Uint63_land(x,y) (accu = (value)((uint64_t)(x) & (uint64_t)(y))) /* TODO: is + or | better? OCAML uses + */ /* TODO: is - or ^ better? */ -#define uint63_lsl(x,y) ((y) < (uint64_t) 127 ? ((value)((((uint64_t)(x)-1) << (uint63_of_value(y))) | 1)) : uint63_zero) -#define uint63_lsr(x,y) ((y) < (uint64_t) 127 ? ((value)(((uint64_t)(x) >> (uint63_of_value(y))) | 1)) : uint63_zero) -#define uint63_lsl1(x) ((value)((((uint64_t)(x)-1) << 1) +1)) -#define uint63_lsr1(x) ((value)(((uint64_t)(x) >> 1) |1)) +#define Uint63_lsl(x,y) do{ \ + value uint63_lsl_y__ = (y); \ + if (uint63_lsl_y__ < (uint64_t) 127) \ + accu = (value)((((uint64_t)(x)-1) << uint63_of_value(uint63_lsl_y__)) | 1); \ + else \ + accu = uint63_zero; \ + }while(0) +#define Uint63_lsr(x,y) do{ \ + value uint63_lsl_y__ = (y); \ + if (uint63_lsl_y__ < (uint64_t) 127) \ + accu = (value)(((uint64_t)(x) >> uint63_of_value(uint63_lsl_y__)) | 1); \ + else \ + accu = uint63_zero; \ + }while(0) +#define Uint63_lsl1(x) (accu = (value)((((uint64_t)(x)-1) << 1) +1)) +#define Uint63_lsr1(x) (accu = (value)(((uint64_t)(x) >> 1) |1)) /* addmuldiv(p,x,y) = x * 2^p + y / 2 ^ (63 - p) */ /* (modulo 2^63) for p <= 63 */ @@ -40,6 +55,7 @@ value uint63_addmuldiv(uint64_t p, uint64_t x, uint64_t y) { r |= ((uint64_t)y >> (63-shiftby)) | 1; return r; } +#define Uint63_addmuldiv(p, x, y) (accu = uint63_addmuldiv(p, x, y)) value uint63_head0(uint64_t x) { int r = 0; @@ -51,6 +67,7 @@ value uint63_head0(uint64_t x) { if (!(x & 0x8000000000000000)) { x <<=1; r += 1; } return Val_int(r); } +#define Uint63_head0(x) (accu = uint63_head0(x)) value uint63_tail0(value x) { int r = 0; @@ -63,6 +80,7 @@ value uint63_tail0(value x) { if (!(x & 0x00000001)) { x >>=1; r += 1; } return Val_int(r); } +#define Uint63_tail0(x) (accu = uint63_tail0(x)) value uint63_mulc(value x, value y, value* h) { x = (uint64_t)x >> 1; @@ -86,6 +104,7 @@ value uint63_mulc(value x, value y, value* h) { *h = Val_int(hr); return Val_int(lr); } +#define Uint63_mulc(x, y, h) (accu = uint63_mulc(x, y, h)) #define lt128(xh,xl,yh,yl) (uint63_lt(xh,yh) || (uint63_eq(xh,yh) && uint63_lt(xl,yl))) #define le128(xh,xl,yh,yl) (uint63_lt(xh,yh) || (uint63_eq(xh,yh) && uint63_leq(xl,yl))) @@ -123,3 +142,4 @@ value uint63_div21(value xh, value xl, value y, value* q) { *q = Val_int(quotient); return Val_int(reml); } +#define Uint63_div21(xh, xl, y, q) (accu = uint63_div21(xh, xl, y, q)) diff --git a/lib/envars.ml b/lib/envars.ml index 0f4670688b..af8e45b137 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -178,6 +178,7 @@ let print_config ?(prefix_var_name="") f coq_src_subdirs = fprintf f "%sDOCDIR=%s/\n" prefix_var_name (docdir ()); fprintf f "%sOCAMLFIND=%s\n" prefix_var_name (ocamlfind ()); fprintf f "%sCAMLFLAGS=%s\n" prefix_var_name Coq_config.caml_flags; + fprintf f "%sWARN=%s\n" prefix_var_name "-warn-error +a-3"; fprintf f "%sHASNATDYNLINK=%s\n" prefix_var_name (if Coq_config.has_natdynlink then "true" else "false"); fprintf f "%sCOQ_SRC_SUBDIRS=%s\n" prefix_var_name (String.concat " " coq_src_subdirs) diff --git a/plugins/funind/plugin_base.dune b/plugins/funind/plugin_base.dune index 002eb28eea..6ccf15df29 100644 --- a/plugins/funind/plugin_base.dune +++ b/plugins/funind/plugin_base.dune @@ -1,5 +1,5 @@ (library (name recdef_plugin) - (public_name coq.plugins.recdef) + (public_name coq.plugins.funind) (synopsis "Coq's functional induction plugin") (libraries coq.plugins.extraction)) diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index bf7f082192..08f028465b 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -465,7 +465,7 @@ let interp_modloc mr = (* The unified, extended vernacular "Search" command *) let ssrdisplaysearch gr env t = - let pr_res = pr_global gr ++ spc () ++ str " " ++ pr_lconstr_env env Evd.empty t in + let pr_res = pr_global gr ++ str ":" ++ spc () ++ pr_lconstr_env env Evd.empty t in Feedback.msg_info (hov 2 pr_res ++ fnl ()) } diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh index 78a3f7c63a..4ee4aae36c 100755 --- a/test-suite/coq-makefile/timing/run.sh +++ b/test-suite/coq-makefile/timing/run.sh @@ -49,16 +49,15 @@ TO_SED_IN_BOTH=( -e s'/[0-9]*\.[0-9]*//g' # the precise timing numbers vary, so we strip them out -e s'/^-*$/------/g' # When none of the numbers get over 100 (or 1000, in per-file), the width of the table is different, so we normalize the number of dashes for table separators -e s'/+/-/g' # some code lines don't really change, but this can show up as either -0m00.01s or +0m00.01s, so we need to normalize the signs; additionally, some N/A's show up where we expect to get -∞ on the per-line file, and so the ∞-replacement gets the sign wrong, so we must correct it + -e s'/[0-9]//g' # sometimes the time is under 1 minute, sometimes it's over 1 minute, so we want to remove/normalize both instances; see https://github.com/coq/coq/issues/5675#issuecomment-487378622 ) TO_SED_IN_PER_FILE=( - -e s'/[0-9]//g' # unclear whether this is actually needed above and beyond s'/[0-9]*\.[0-9]*//g'; it's been here from the start -e s'/ */ /g' # unclear whether this is actually needed for per-file timing; it's been here from the start -e s'/\(Total.*\)-\(.*\)-/\1+\2+/g' # Overall time in the per-file timing diff should be around 0; if it comes out negative, we remove the sign ) TO_SED_IN_PER_LINE=( - -e s'/0//g' # unclear whether this is actually needed above and beyond s'/[0-9]*\.[0-9]*//g'; it's been here from the start -e s'/ */ /g' # Sometimes 0 will show up as 0m00.s, sometimes it'll end up being more like 0m00.001s; we must strip out the spaces that result from left-aligning numbers of different widths based on how many digits Coq's [-time] gives ) diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 0236c549d5..2ec55d1bd0 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -38,6 +38,7 @@ DOCDIR := $(COQMF_DOCDIR) OCAMLFIND := $(COQMF_OCAMLFIND) CAMLFLAGS := $(COQMF_CAMLFLAGS) HASNATDYNLINK := $(COQMF_HASNATDYNLINK) +OCAMLWARN := $(COQMF_WARN) @CONF_FILE@: @PROJECT_FILE@ @COQ_MAKEFILE_INVOCATION@ @@ -176,7 +177,7 @@ COQCHKEXTRAFLAGS?= COQDOCEXTRAFLAGS?= # these flags do NOT contain the libraries, to make them easier to overwrite -COQFLAGS?=-q $(OPT) $(OTHERFLAGS) $(COQEXTRAFLAGS) +COQFLAGS?=-q $(OTHERFLAGS) $(COQEXTRAFLAGS) COQCHKFLAGS?=-silent -o $(COQCHKEXTRAFLAGS) COQDOCFLAGS?=-interpolate -utf8 $(COQDOCEXTRAFLAGS) @@ -190,9 +191,9 @@ COQMAKEFILE_VERSION:=@COQ_VERSION@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)") CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) - # ocamldoc fails with unknown argument otherwise -CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) +CAMLDOCFLAGS:=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) +CAMLFLAGS+=$(OCAMLWARN) ifneq (,$(TIMING)) TIMING_ARG=-time diff --git a/topbin/dune b/topbin/dune index e35a3de54b..3b861afe78 100644 --- a/topbin/dune +++ b/topbin/dune @@ -28,6 +28,11 @@ (libraries coq.toplevel) (link_flags -linkall)) +(install + (section bin) + (package coq) + (files (coqc_bin.bc as coqc.byte))) + ; Workers (executables (names coqqueryworker_bin coqtacticworker_bin coqproofworker_bin) |