Commit c01d406b9b8470cfd1eb1804182b9620f9425b95 - coq

+5

-0

.github/workflows/check-conflicts.yml less more

2	2	# Only on push because @coqbot already takes care of checking for
3	3	# conflicts when PRs are opened or synchronized
4	4
	5	permissions:
	6	contents: read
	7
5	8	jobs:
6	9	main:
	10	permissions:
	11	pull-requests: write
7	12	runs-on: ubuntu-latest
8	13	steps:
9	14	- uses: eps1lon/actions-label-merge-conflict@b8bf8341285ec9a4567d4318ba474fee998a6919

+1

-1

.github/workflows/ci-macos.yml less more

9	9	runs-on: macOS-10.15
10	10
11	11	steps:
12		- uses: actions/checkout@v2
	12	- uses: actions/checkout@v3
13	13
14	14	- name: Install system dependencies
15	15	run: \|

+4

-3

.github/workflows/ci-windows.yml less more

22	22	git config --global core.eol lf
23	23
24	24	- name: Git checkout
25		uses: actions/checkout@v2
	25	uses: actions/checkout@v3
26	26
27	27	- name: System Information
28	28	run: \|

30	30
31	31	- name: Download Platform
32	32	env:
33		PLATFORM: "https://github.com/coq/platform/archive/2022.04.0.zip"
	33	# Use a dedicated branch that follows master with some lag (manually updated)
	34	PLATFORM: "https://github.com/coq/platform/archive/coq-ci.zip"
34	35	run: \|
35	36	.\dev\ci\platform\coq-pf-02-download.bat
36	37

49	50	.\dev\ci\platform\coq-pf-04-installer.bat
50	51
51	52	- name: Upload Installer
52		uses: actions/upload-artifact@v2
	53	uses: actions/upload-artifact@v3
53	54	with:
54	55	name: windows-installer
55	56	path: artifacts

+2

-0

.gitlab-ci.yml less more

815	815
816	816	library:ci-vst:
817	817	extends: .ci-template-flambda
	818	variables:
	819	NJOBS: "1"
818	820	needs:
819	821	- build:edge+flambda
820	822	- library:ci-flocq3

+1

-1

coq-doc.opam less more

10	10	This package provides the Coq Reference Manual."""
11	11	maintainer: ["The Coq development team <coqdev@inria.fr>"]
12	12	authors: ["The Coq development team, INRIA, CNRS, and contributors"]
13		license: "OPL-1.0"
	13	license: "OPUBL-1.0"
14	14	homepage: "https://coq.inria.fr/"
15	15	doc: "https://coq.github.io/doc/"
16	16	bug-reports: "https://github.com/coq/coq/issues"

+1

-0

dev/ci/user-overlays/16434-SkySkimmer-assumptions-vos.sh less more

0

overlay paramcoq https://github.com/SkySkimmer/paramcoq assumptions-vos 16434

+31

-0

dev/doc/critical-bugs less more

385	385	risk: none, unless mixing open terms and primitive floats inside primitive
386	386	arrays; critical otherwise
387	387
	388	component: "native" conversion machine (translation to OCaml which compiles to native code)
	389	summary: conversion of Prod / Prod values was comparing the wrong components
	390	introduced: V8.5
	391	impacted released versions: V8.5-V8.16.0 (when built with native computation enabled)
	392	impacted coqchk versions: none (no native computation in coqchk)
	393	fixed in: 8.16.1
	394	found by: Melquiond
	395	GH issue number: #16645
	396	risk: systematic
	397
	398	component: "virtual" and "native" conversion machines
	399	summary: η-expansion of cofixpoints was performed in the wrong environment
	400	introduced: V8.9
	401	impacted released versions: V8.9-V8.16.0
	402	impacted coqchk versions: none (no VM / native computation in coqchk)
	403	fixed in: 8.16.1
	404	found by: Gaëtan Gilbert and Pierre-Marie Pédrot
	405	GH issue number: #16831
	406	risk: low, as it requires carefully crafted cofixpoints
	407
	408	component: all 3 kernel conversion machines (lazy, VM, native), primitive arrays
	409	summary: conversion would compare the mutated version of primitive arrays instead of undoing mutation where needed
	410	introduced: V8.13
	411	impacted released versions: V8.13 to V8.16.0
	412	impacted coqchk versions: same
	413	fixed in: V8.16.1, V8.17
	414	found by: Maxime Buyse and Andres Erbsen
	415	exploit: Andres Erbsen
	416	GH issue number: #16829
	417	risk: some if using primitive arrays
	418
388	419	Side-effects
389	420
390	421	component: side-effects

+1

-1

dune-project less more

95	95
96	96	(package
97	97	(name coq-doc)
98		(license "OPL-1.0")
	98	(license "OPUBL-1.0")
99	99	(depends
100	100	(dune (and :build (>= 2.5.0)))
101	101	(conf-python-3 :build)

+1

-0

ide/coqide/coq.ml less more

171	171	let mk_ccb poly = { open_ccb = fun scope -> scope.bind_ccb poly }
172	172	let with_ccb ccb e = ccb.open_ccb e
173	173
	174	(* overridden on Windows; see file coqide_WIN32.c.in *)
174	175	let interrupter = ref (fun pid -> Unix.kill pid Sys.sigint)
175	176
176	177	(* todo: does not work on windows (sigusr1 not supported) *)

+6

-1

ide/coqide/coqide.ml less more

441	441	end)
442	442	notebook#pages
443	443
	444	let win_interrupt = ref false
	445
444	446	let quit ?parent _ =
445		if not !FileAux.in_quit_dialog then
	447	if !win_interrupt then
	448	win_interrupt := false
	449	else if not !FileAux.in_quit_dialog then
446	450	try FileAux.check_quit ?parent saveall; exit 0
447	451	with FileAux.DontQuit -> ()
448	452

841	845	Coq.reset_coqtop sn.coqtop (* calls init_bpts *)
842	846	end
843	847	let interrupt _ = (* terminate computation *)
	848	if Sys.os_type = "Win32" then File.win_interrupt := true;
844	849	Minilib.log "User interrupt received";
845	850	if not (resume_debugger Interface.Interrupt) && notebook#pages <> [] then begin
846	851	let osn = (find_db_sn ()) in

+8

-20

ide/coqide/coqide_WIN32.c.in less more

5	5
6	6	/* Win32 emulation of a kill -2 (SIGINT) */
7	7
8		/* This code rely of the fact that coqide is now without initial console.
9		Otherwise, no console creation in win32unix/createprocess.c, hence
10		the same console for coqide and all coqtop, and everybody will be
11		signaled at the same time by the code below. */
12
13		/* Moreover, AttachConsole exists only since WinXP, and GetProcessId
14		since WinXP SP1. For avoiding the GetProcessId, we could adapt code
15		from win32unix/createprocess.c to make it return both the pid and the
16		handle. For avoiding the AttachConsole, I don't know, maybe having
17		an intermediate process between coqide and coqtop ? */
	8	/* It appears that the documentation for SetConsoleCtrlHandler used in the
	9	prior code (f5276a11) is incorrect. When it's present, it causes some of
	10	the strange behavior described in #13550.
	11
	12	This code signals all processes in the process group (multiple coqidetops) and coqide.
	13	because the console is shared. Coqide.win_interrupt is used to ignore the signal sent
	14	to CoqIDE. */
18	15
19	16	CAMLprim value win32_interrupt(value pseudopid) {
20	17	CAMLparam1(pseudopid);
21		HANDLE h;
22		DWORD pid;
23		FreeConsole(); /* Normally unnecessary, just to be sure... */
24		h = (HANDLE)(Long_val(pseudopid));
25		pid = GetProcessId(h);
26		AttachConsole(pid);
27		/* We want to survive the Ctrl-C that will also concerns us */
28		SetConsoleCtrlHandler(NULL,TRUE); /* NULL + TRUE means ignore */
29		GenerateConsoleCtrlEvent(CTRL_C_EVENT,0); /* signal our co-console */
30		FreeConsole();
	18	GenerateConsoleCtrlEvent(CTRL_C_EVENT,0); /* signal each process in the process group */
31	19	CAMLreturn(Val_unit);
32	20	}

+7

-1

ide/coqide/coqide_WIN32.ml.in less more

40	40
41	41	external win32_interrupt : int -> unit = "win32_interrupt"
42	42
	43	let interrupter pid =
	44	(* indicate which process to interrupt *)
	45	let fd = open_out (Shared.get_interrupt_fname pid) in
	46	close_out fd;
	47	win32_interrupt pid
	48
43	49	let () =
44	50	Coq.gio_channel_of_descr_socket := Glib.Io.channel_of_descr_socket;
45	51	set_win32_path ();
46		Coq.interrupter := win32_interrupt;
	52	Coq.interrupter := interrupter;
47	53	reroute_stdout_stderr ();
48	54	try ignore (Unix.getenv "GTK_CSD") with Not_found -> Unix.putenv "GTK_CSD" "0"
49	55

+1

-0

ide/coqide/coqide_main.ml less more

62	62	let w = Coqide.main files in
63	63	Coqide.set_signal_handlers ~parent:w ();
64	64	Coqide_os_specific.init ();
	65	Shared_os_specific.init ();
65	66	try
66	67	GMain.main ();
67	68	failwith "Gtk loop ended"

+21

-3

ide/coqide/dune less more

12	12	(public_name coqidetop.opt)
13	13	(package coqide-server)
14	14	(modules idetop)
15		(libraries coq-core.toplevel coqide-server.protocol)
	15	(libraries coq-core.toplevel coqide-server.protocol platform_specific)
16	16	(modes native byte)
17	17	(link_flags -linkall))
18	18

25	25	(library
26	26	(name coqide_gui)
27	27	(wrapped false)
28		(modules (:standard \ document idetop coqide_main default_bindings_src gen_gtk_platform))
	28	(modules (:standard \ document idetop coqide_main default_bindings_src gen_gtk_platform
	29	shared shared_os_specific))
29	30	(foreign_stubs
30	31	(language c)
31	32	(names coqide_os_stubs))
32	33	(optional)
33		(libraries coqide-server.protocol coqide-server.core lablgtk3-sourceview3))
	34	(libraries coqide-server.protocol coqide-server.core lablgtk3-sourceview3 platform_specific))
	35
	36	(library
	37	(name platform_specific)
	38	(wrapped false)
	39	(modules shared shared_os_specific)
	40	(foreign_stubs
	41	(language c)
	42	(names shared_os_stubs))
	43	)
34	44
35	45	(executable
36	46	(name gen_gtk_platform)

46	56	(action (copy# coqide_%{read:gtk_platform.conf}.ml.in %{targets})))
47	57
48	58	(rule
	59	(targets shared_os_specific.ml)
	60	(action (copy# shared_%{read:gtk_platform.conf}.ml.in %{targets})))
	61
	62	(rule
49	63	(targets coqide_os_stubs.c)
50	64	(action (copy coqide_%{read:gtk_platform.conf}.c.in %{targets})))
	65
	66	(rule
	67	(targets shared_os_stubs.c)
	68	(action (copy shared_%{read:gtk_platform.conf}.c.in %{targets})))
51	69
52	70	(executable
53	71	(name coqide_main)

+13

-1

ide/coqide/idetop.ml less more

26	26
27	27	let catch_break = ref false
28	28
	29	(* tell whether we have a bona fide interrupt *)
	30	let valid_interrupt () =
	31	if Sys.os_type = "Win32" then begin
	32	let fname = Shared.get_interrupt_fname (Unix.getpid ()) in
	33	let exists = Sys.file_exists fname in
	34	if exists then Unix.unlink fname;
	35	exists
	36	end else
	37	true
	38
29	39	let init_signal_handler () =
30		let f _ = if !catch_break then raise Sys.Break else Control.interrupt := true in
	40	let f _ = if valid_interrupt () then
	41	if !catch_break then raise Sys.Break else Control.interrupt := true in
31	42	Sys.set_signal Sys.sigint (Sys.Signal_handle f)
32	43
33	44	let pr_with_pid s = Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s

691	702
692	703	let () =
693	704	let open Coqtop in
	705	Shared_os_specific.init ();
694	706	let custom = {
695	707	parse_extra = islave_parse ;
696	708	usage = coqidetop_specific_usage;

+34

-5

ide/coqide/preferences.ml less more

665	665	let pref_file = Filename.concat (Minilib.coqide_config_home ()) "coqiderc"
666	666	let accel_file = Filename.concat (Minilib.coqide_config_home ()) "coqide.keys"
667	667
	668	(* Attention: this only works with absolute normalized paths -
	669	which can be assumed here since the path comes from Glib.get_user_config_dir *)
	670	let rec mkdir_p path perms =
	671	if not (Sys.file_exists path)
	672	then
	673	let parent = Filename.dirname path in
	674	if not (Sys.file_exists parent) && parent<>path
	675	then mkdir_p parent perms
	676	else Unix.mkdir path perms
	677	else ()
	678
668	679	let save_accel_pref () =
669		if not (Sys.file_exists (Minilib.coqide_config_home ()))
670		then Unix.mkdir (Minilib.coqide_config_home ()) 0o700;
	680	mkdir_p (Minilib.coqide_config_home ()) 0o700;
671	681	GtkData.AccelMap.save accel_file
672	682
673	683	let save_rc_pref () =
674		if not (Sys.file_exists (Minilib.coqide_config_home ()))
675		then Unix.mkdir (Minilib.coqide_config_home ()) 0o700;
	684	mkdir_p (Minilib.coqide_config_home ()) 0o700;
676	685	let add = Util.String.Map.add in
677	686	let fold key obj accu = add key (obj.get ()) accu in
678	687	let prefs = Util.String.Map.fold fold !preferences Util.String.Map.empty in

748	757	let cmd_coqdoc = pstring " coqdoc" cmd_coqdoc in
749	758	let cmd_print = pstring " Print ps" cmd_print in
750	759
751		let config_font =
	760	let config_font = match Coq_config.arch with
	761	\| "Darwin" ->
	762	(* A poor man's font selection. Work around #16136, which is ultimately a GTK bug. *)
	763	let box = GPack.vbox () in
	764	let () = box#set_height_request 200 in
	765	let () = box#set_height_request 300 in
	766	let w = GEdit.entry ~text:text_font#get () in
	767	let () = box#pack ~expand:false w#coerce in
	768	let text = GMisc.label ~text:"Goal (∃n : nat, n ≤ 0)∧(∀x,y,z, x∈y⋃z↔x∈y∨x∈z)." () in
	769	let () = text#set_ypad 10 in
	770	let () = box#pack ~expand:false text#coerce in
	771	let set_font () =
	772	let fd = GPango.font_description_from_string w#text in
	773	let () = text_font#set fd#to_string in
	774	let () = text#misc#modify_font_by_name fd#to_string in
	775	w#set_text fd#to_string
	776	in
	777	let () = text#misc#modify_font_by_name text_font#get in
	778	let _ = w#connect#activate ~callback:set_font in
	779	custom ~label:"Fonts for text" box set_font true
	780	\| _ ->
752	781	let box = GPack.hbox () in
753	782	let w = GMisc.font_selection () in
754	783	w#set_preview_text

+16

-0

ide/coqide/shared.ml less more

	0	(************************************************************************)
	1	(* * The Coq Proof Assistant / The Coq Development Team *)
	2	(* v * Copyright INRIA, CNRS and contributors *)
	3	(* <O___,, * (see version control and CREDITS file for authors & dates) *)
	4	(* \VV/ **************************************************************)
	5	(* // * This file is distributed under the terms of the *)
	6	(* * GNU Lesser General Public License Version 2.1 *)
	7	(* * (see LICENSE file for the text of the license) *)
	8	(************************************************************************)
	9
	10	(* overridden on Windows; see file shared_WIN32.c.in *)
	11	let cvt_pid = ref (fun pid -> pid)
	12
	13	let get_interrupt_fname pid =
	14	Filename.concat (Filename.get_temp_dir_name ())
	15	(Printf.sprintf "coqide_interrupt_%d" (!cvt_pid pid))

+15

-0

ide/coqide/shared.mli less more

	0	(************************************************************************)
	1	(* * The Coq Proof Assistant / The Coq Development Team *)
	2	(* v * Copyright INRIA, CNRS and contributors *)
	3	(* <O___,, * (see version control and CREDITS file for authors & dates) *)
	4	(* \VV/ **************************************************************)
	5	(* // * This file is distributed under the terms of the *)
	6	(* * GNU Lesser General Public License Version 2.1 *)
	7	(* * (see LICENSE file for the text of the license) *)
	8	(************************************************************************)
	9
	10	val get_interrupt_fname : int -> string
	11	(** get filename used to pass interrupt pid on Win32 *)
	12
	13	val cvt_pid : (int -> int) ref
	14	(* On Win32, convert OCaml "pid" (a handle) to a genuine Win32 pid *)

+1

-0

ide/coqide/shared_QUARTZ.c.in less more

0

/* no osx-specific stubs for now */

+11

-0

ide/coqide/shared_QUARTZ.ml.in less more

	0	(************************************************************************)
	1	(* * The Coq Proof Assistant / The Coq Development Team *)
	2	(* v * Copyright INRIA, CNRS and contributors *)
	3	(* <O___,, * (see version control and CREDITS file for authors & dates) *)
	4	(* \VV/ **************************************************************)
	5	(* // * This file is distributed under the terms of the *)
	6	(* * GNU Lesser General Public License Version 2.1 *)
	7	(* * (see LICENSE file for the text of the license) *)
	8	(************************************************************************)
	9
	10	let init () = ()

+16

-0

ide/coqide/shared_WIN32.c.in less more

	0	#define _WIN32_WINNT 0x0501 /* Cf below, we restrict to */
	1
	2	#include <caml/mlvalues.h>
	3	#include <caml/memory.h>
	4	#include <windows.h>
	5
	6	/* convert an OCaml pid (a process-local handle #) to a Win32 pid (global) */
	7	CAMLprim value win32_cvtpid(value pseudopid) {
	8	CAMLparam1(pseudopid);
	9	HANDLE h;
	10	DWORD win32_pid;
	11
	12	h = (HANDLE)(Long_val(pseudopid));
	13	win32_pid = GetProcessId(h);
	14	CAMLreturn(Val_int(win32_pid));
	15	}

+16

-0

ide/coqide/shared_WIN32.ml.in less more

	0	(************************************************************************)
	1	(* * The Coq Proof Assistant / The Coq Development Team *)
	2	(* v * Copyright INRIA, CNRS and contributors *)
	3	(* <O___,, * (see version control and CREDITS file for authors & dates) *)
	4	(* \VV/ **************************************************************)
	5	(* // * This file is distributed under the terms of the *)
	6	(* * GNU Lesser General Public License Version 2.1 *)
	7	(* * (see LICENSE file for the text of the license) *)
	8	(************************************************************************)
	9
	10	external win32_cvtpid : int -> int = "win32_cvtpid"
	11
	12	let () =
	13	Shared.cvt_pid := win32_cvtpid
	14
	15	let init () = ()

+1

-0

ide/coqide/shared_X11.c.in less more

0

/* no Linux-specific stubs for now */

+11

-0

ide/coqide/shared_X11.ml.in less more

	0	(************************************************************************)
	1	(* * The Coq Proof Assistant / The Coq Development Team *)
	2	(* v * Copyright INRIA, CNRS and contributors *)
	3	(* <O___,, * (see version control and CREDITS file for authors & dates) *)
	4	(* \VV/ **************************************************************)
	5	(* // * This file is distributed under the terms of the *)
	6	(* * GNU Lesser General Public License Version 2.1 *)
	7	(* * (see LICENSE file for the text of the license) *)
	8	(************************************************************************)
	9
	10	let init () = ()

+11

-0

ide/coqide/shared_os_specific.mli less more

	0	(************************************************************************)
	1	(* * The Coq Proof Assistant / The Coq Development Team *)
	2	(* v * Copyright INRIA, CNRS and contributors *)
	3	(* <O___,, * (see version control and CREDITS file for authors & dates) *)
	4	(* \VV/ **************************************************************)
	5	(* // * This file is distributed under the terms of the *)
	6	(* * GNU Lesser General Public License Version 2.1 *)
	7	(* * (see LICENSE file for the text of the license) *)
	8	(************************************************************************)
	9
	10	val init : unit -> unit

+8

-4

kernel/byterun/coq_interp.c less more

924	924	mlsize_t i;
925	925	value block;
926	926	print_instr("MAKEBLOCK, tag=");
927		Coq_alloc_small(block, wosize, tag);
928		Field(block, 0) = accu;
929		for (i = 1; i < wosize; i++) Field(block, i) = *sp++;
930		accu = block;
	927	if (wosize == 0) {
	928	accu = Atom(tag);
	929	} else {
	930	Coq_alloc_small(block, wosize, tag);
	931	Field(block, 0) = accu;
	932	for (i = 1; i < wosize; i++) Field(block, i) = *sp++;
	933	accu = block;
	934	}
931	935	Next;
932	936	}
933	937	Instruct(MAKEBLOCK1) {

+24

-21

kernel/cClosure.ml less more

523	523	let shortcut_irrelevant mode r =
524	524	if is_irrelevant mode r then raise Irrelevant
525	525
526		let assoc_defined mode id env = match Environ.lookup_named id env with
527		\| LocalDef (na, c, _) ->
528		let () = shortcut_irrelevant mode (binder_relevance na) in
529		c
530		\| LocalAssum (na, _) ->
531		let () = shortcut_irrelevant mode (binder_relevance na) in
532		raise Not_found
533
534		let constant_value_in mode env (kn, u) =
535		let cb = lookup_constant kn env in
536		let () = shortcut_irrelevant mode (cb.const_relevance) in
537		match cb.const_body with
538		\| Def b -> subst_instance_constr u b
539		\| OpaqueDef _ -> raise (NotEvaluableConst Opaque)
540		\| Undef _ -> raise (NotEvaluableConst NoBody)
541		\| Primitive p -> raise (NotEvaluableConst (IsPrimitive (u,p)))
	526	let assoc_defined = function
	527	\| LocalDef (_, c, _) -> c
	528	\| LocalAssum (_, _) -> raise Not_found
	529
	530	let constant_value_in u = function
	531	\| Def b -> subst_instance_constr u b
	532	\| OpaqueDef _ -> raise (NotEvaluableConst Opaque)
	533	\| Undef _ -> raise (NotEvaluableConst NoBody)
	534	\| Primitive p -> raise (NotEvaluableConst (IsPrimitive (u,p)))
542	535
543	536	let ref_value_cache env flags mode tab ref =
544	537	try

562	555	\| LocalDef (_, t, _) -> lift n t
563	556	end
564	557	\| VarKey id ->
565		if TransparentState.is_transparent_variable flags id then assoc_defined mode id env
	558	let def = Environ.lookup_named id env in
	559	let () = shortcut_irrelevant mode (binder_relevance (get_annot def)) in
	560	if TransparentState.is_transparent_variable flags id then assoc_defined def
566	561	else raise Not_found
567		\| ConstKey cst ->
568		if TransparentState.is_transparent_constant flags (fst cst) then constant_value_in mode env cst
	562	\| ConstKey (cst,u) ->
	563	let cb = lookup_constant cst env in
	564	let () = shortcut_irrelevant mode (cb.const_relevance) in
	565	if TransparentState.is_transparent_constant flags cst then constant_value_in u cb.const_body
569	566	else raise Not_found
570	567	in
571	568	Def (inject body)

1633	1630	\| FEvar((i,args),env) ->
1634	1631	mkEvar(i, List.map (fun a -> klt info tab env a) args)
1635	1632	\| FProj (p,c) ->
1636		mkProj (p, kl info tab c)
	1633	mkProj (p, kl info tab c)
	1634	\| FArray (u, a, ty) ->
	1635	let a, def = Parray.to_array a in
	1636	let a = Array.map (kl info tab) a in
	1637	let def = kl info tab def in
	1638	let ty = kl info tab ty in
	1639	mkArray (u, a, def, ty)
1637	1640	\| FLOCKED \| FRel _ \| FAtom _ \| FFlex _ \| FInd _ \| FConstruct _
1638	1641	\| FApp _ \| FCaseT _ \| FCaseInvert _ \| FLIFT _ \| FCLOS _ \| FInt _
1639		\| FFloat _ \| FArray _ -> term_of_fconstr m
	1642	\| FFloat _ -> term_of_fconstr m
1640	1643	\| FIrrelevant -> assert false (* only introduced when converting *)
1641	1644
1642	1645	and zip_term info tab m stk = match stk with

+2

-2

kernel/nativeconv.ml less more

117	117	else
118	118	if not (Int.equal (Array.length f1) (Array.length f2)) then raise NotConvertible
119	119	else conv_fix env lvl t1 f1 t2 f2 cu
120		\| Aprod(_,d1,_c1), Aprod(_,d2,_c2) ->
	120	\| Aprod(_,d1,c1), Aprod(_,d2,c2) ->
121	121	let cu = conv_val env CONV lvl d1 d2 cu in
122	122	let v = mk_rel_accu lvl in
123		conv_val env pb (lvl + 1) (d1 v) (d2 v) cu
	123	conv_val env pb (lvl + 1) (c1 v) (c2 v) cu
124	124	\| Aproj((ind1, i1), ac1), Aproj((ind2, i2), ac2) ->
125	125	if not (Ind.CanOrd.equal ind1 ind2 && Int.equal i1 i2) then raise NotConvertible
126	126	else conv_accu env CONV lvl ac1 ac2 cu

+2

-1

kernel/nativelambda.ml less more

590	590	Lfix((pos, inds, i), (names, ltypes, lbodies))
591	591
592	592	\| CoFix(init,(names,type_bodies,rec_bodies)) ->
593		let rec_bodies = Array.map2 (Reduction.eta_expand env) rec_bodies type_bodies in
594	593	let ltypes = lambda_of_args cache env sigma 0 type_bodies in
595	594	let env = Environ.push_rec_types (names, type_bodies, rec_bodies) env in
	595	let map c ty = Reduction.eta_expand env c (Vars.lift (Array.length type_bodies) ty) in
	596	let rec_bodies = Array.map2 map rec_bodies type_bodies in
596	597	let lbodies = lambda_of_args cache env sigma 0 rec_bodies in
597	598	Lcofix(init, (names, ltypes, lbodies))
598	599

+55

-31

kernel/parray.ml less more

133	133	\| Array (_,def) -> def
134	134	\| Updated _ -> assert false
135	135
136		let make n def =
137		ref (Array (UArray.make (trunc_size n) def, def))
	136	let make_int n def =
	137	ref (Array (UArray.make n def, def))
	138
	139	let make n def = make_int (trunc_size n) def
138	140
139	141	let uinit n f =
140	142	if Int.equal n 0 then UArray.empty

163	165	\| Array (t, def) -> ref (Array (UArray.copy t, def))
164	166	\| Updated _ -> assert false
165	167
166		let reroot t =
167		let _ = reroot t in
168		t
	168	(* Higher order combinators: the callback may update the underlying
	169	array requiring a reroot between each call. To avoid doing n
	170	reroots (-> O(n^2)), we copy if we have to reroot again. *)
	171
	172	let is_rooted p = match !p with
	173	\| Array _ -> true
	174	\| Updated _ -> false
	175
	176	type 'a cache = {
	177	orig : 'a t;
	178	mutable self : 'a UArray.t;
	179	mutable rerooted_again : bool;
	180	}
	181
	182	let make_cache p = {
	183	orig = p;
	184	self = reroot p;
	185	rerooted_again = false;
	186	}
	187
	188	let uget_cache cache i =
	189	let () = if not cache.rerooted_again && not (is_rooted cache.orig)
	190	then begin
	191	cache.self <- UArray.copy (reroot cache.orig);
	192	cache.rerooted_again <- true
	193	end
	194	in
	195	UArray.unsafe_get cache.self i
169	196
170	197	let map f p =
171		let p = reroot p in
172		match !p with
173		\| Array (t,def) ->
174		let t = uinit (UArray.length t) (fun i -> f (UArray.unsafe_get t i)) in
175		ref (Array (t, f def))
176		\| Updated _ -> assert false
	198	let t = make_cache p in
	199	let len = UArray.length t.self in
	200	let res = uinit len (fun i -> f (uget_cache t i)) in
	201	let def = f (default p) in
	202	ref (Array (res, def))
177	203
178	204	let fold_left f x p =
179		let p = reroot p in
180		match !p with
181		\| Array (t,def) ->
182		let r = ref x in
183		for i = 0 to UArray.length t - 1 do
184		r := f !r (UArray.unsafe_get t i)
185		done;
186		f !r def
187		\| Updated _ -> assert false
	205	let r = ref x in
	206	let t = make_cache p in
	207	let len = UArray.length t.self in
	208	for i = 0 to len - 1 do
	209	r := f !r (uget_cache t i)
	210	done;
	211	f !r (default p)
188	212
189	213	let fold_left2 f a p1 p2 =
190		let p1 = reroot p1 in
191		let p2 = reroot p2 in
192		match !p1, !p2 with
193		\| Array (t1, def1), Array (t2, def2) ->
194		if UArray.length t1 <> UArray.length t2 then invalid_arg "Array.fold_left2";
195		let r = ref a in
196		for i = 0 to UArray.length t1 - 1 do
197		r := f !r (UArray.unsafe_get t1 i) (UArray.unsafe_get t2 i)
198		done;
199		f !r def1 def2
200		\| _ -> assert false
	214	let r = ref a in
	215	let t1 = make_cache p1 in
	216	let len = UArray.length t1.self in
	217	let t2 = make_cache p2 in
	218	if UArray.length t2.self <> len then invalid_arg "Parray.fold_left2";
	219	for i = 0 to len - 1 do
	220	let v1 = uget_cache t1 i in
	221	let v2 = uget_cache t2 i in
	222	r := f !r v1 v2
	223	done;
	224	f !r (default p1) (default p2)

+2

-1

kernel/vmbytegen.ml less more

754	754	\| Lmakeblock (tag,args) ->
755	755	let arity = Array.length args in
756	756	let cont = code_makeblock ~stack_size:(sz+arity-1) ~arity ~tag cont in
757		comp_args (compile_lam env) cenv args sz cont
	757	if Int.equal arity 0 then cont
	758	else comp_args (compile_lam env) cenv args sz cont
758	759
759	760	\| Lprim (kn, op, args) ->
760	761

+1

-2

kernel/vmemitcodes.ml less more

334	334	\| Kconst c ->
335	335	out env opGETGLOBAL; slot_for_const env c
336	336	\| Kmakeblock(n, t) ->
337		if Int.equal n 0 then invalid_arg "emit_instr : block size = 0"
338		else if n < 4 then (out env(opMAKEBLOCK1 + n - 1); out_int env t)
	337	if 0 < n && n < 4 then (out env(opMAKEBLOCK1 + n - 1); out_int env t)
339	338	else (out env opMAKEBLOCK; out_int env n; out_int env t)
340	339	\| Kmakeswitchblock(typlbl,swlbl,annot,sz) ->
341	340	out env opMAKESWITCHBLOCK;

+35

-83

kernel/vmlambda.ml less more

8	8	open Pp
9	9
10	10	let pr_con sp = str(Names.Label.to_string (Constant.label sp))
	11
	12	module RelDecl = Context.Rel.Declaration
11	13
12	14	type lambda =
13	15	\| Lrel of Name.t * int

536	538	let decl = Array.of_list decl in
537	539	Array.map fst decl
538	540
539
540		(* Rel Environment *)
541		module Vect =
542		struct
543		type 'a t = {
544		mutable elems : 'a array;
545		mutable size : int;
546		}
547
548		let make n a = {
549		elems = Array.make n a;
550		size = 0;
551		}
552
553		let extend (v : 'a t) =
554		if v.size = Array.length v.elems then
555		let new_size = min (2*v.size) Sys.max_array_length in
556		if new_size <= v.size then raise (Invalid_argument "Vect.extend");
557		let new_elems = Array.make new_size v.elems.(0) in
558		Array.blit v.elems 0 new_elems 0 (v.size);
559		v.elems <- new_elems
560
561		let push v a =
562		extend v;
563		v.elems.(v.size) <- a;
564		v.size <- v.size + 1
565
566		let popn (v : 'a t) n =
567		v.size <- max 0 (v.size - n)
568
569		let pop v = popn v 1
570
571		let get_last (v : 'a t) n =
572		if v.size <= n then raise
573		(Invalid_argument "Vect.get:index out of bounds");
574		v.elems.(v.size - n - 1)
575
576		end
577
578	541	let dummy_lambda = Lrel(Anonymous, 0)
579	542
580	543	let empty_args = [\|\|]

585	548	type constructor_info = tag * int * int (* nparam nrealargs *)
586	549
587	550	type t = {
588		global_env : env;
	551	env : env;
589	552	evar_body : existential -> constr option;
590		name_rel : Name.t Vect.t;
591	553	construct_tbl : (constructor, constructor_info) Hashtbl.t;
592	554	}
593	555
594	556	let make env sigma = {
595		global_env = env;
	557	env = env;
596	558	evar_body = sigma;
597		name_rel = Vect.make 16 Anonymous;
598	559	construct_tbl = Hashtbl.create 111
599	560	}
600	561
601		let push_rel env id = Vect.push env.name_rel id.Context.binder_name
602
603		let push_rels env ids =
604		Array.iter (push_rel env) ids
605
606		let pop env = Vect.pop env.name_rel
607
608		let popn env n =
609		for _i = 1 to n do pop env done
	562	let push_rel env decl = { env with env = Environ.push_rel decl env.env }
	563
	564	let push_rels env decls = { env with env = Environ.push_rel_context decls env.env }
	565
	566	let push_rec_types env rect = { env with env = Environ.push_rec_types rect env.env }
610	567
611	568	let get env n =
612		Lrel (Vect.get_last env.name_rel (n-1), n)
	569	let na = RelDecl.get_name @@ Environ.lookup_rel n env.env in
	570	Lrel (na, n)
613	571
614	572	let get_construct_info env c =
615	573	try Hashtbl.find env.construct_tbl c
616	574	with Not_found ->
617	575	let ((mind,j), i) = c in
618		let oib = lookup_mind mind env.global_env in
	576	let oib = lookup_mind mind env.env in
619	577	let oip = oib.mind_packets.(j) in
620	578	check_compilable oip;
621	579	let tag,arity = oip.mind_reloc_tbl.(i-1) in

649	607
650	608	\| Prod(id, dom, codom) ->
651	609	let ld = lambda_of_constr env dom in
652		Renv.push_rel env id;
653		let lc = lambda_of_constr env codom in
654		Renv.pop env;
	610	let nenv = Renv.push_rel env (RelDecl.LocalAssum (id, dom)) in
	611	let lc = lambda_of_constr nenv codom in
655	612	Lprod(ld, Llam([\|id\|], lc))
656	613
657	614	\| Lambda _ ->
658	615	let params, body = decompose_lam c in
659		let ids = get_names (List.rev params) in
660		Renv.push_rels env ids;
661		let lb = lambda_of_constr env body in
662		Renv.popn env (Array.length ids);
663		mkLlam ids lb
664
665		\| LetIn(id, def, _, body) ->
	616	let decls = List.map (fun (id, dom) -> RelDecl.LocalAssum (id, dom)) params in
	617	let nenv = Renv.push_rels env decls in
	618	let lb = lambda_of_constr nenv body in
	619	mkLlam (get_names (List.rev params)) lb
	620
	621	\| LetIn(id, def, ty, body) ->
666	622	let ld = lambda_of_constr env def in
667		Renv.push_rel env id;
668		let lb = lambda_of_constr env body in
669		Renv.pop env;
	623	let nenv = Renv.push_rel env (RelDecl.LocalDef (id, def, ty)) in
	624	let lb = lambda_of_constr nenv body in
670	625	Llet(id, ld, lb)
671	626
672	627	\| App(f, args) -> lambda_of_app env f args

676	631	\| Construct _ -> lambda_of_app env c empty_args
677	632
678	633	\| Case (ci, u, pms, t, iv, a, br) -> (* XXX handle iv *)
679		let (ci, t, _iv, a, branches) = Inductive.expand_case env.global_env (ci, u, pms, t, iv, a, br) in
	634	let (ci, t, _iv, a, branches) = Inductive.expand_case env.env (ci, u, pms, t, iv, a, br) in
680	635	let ind = ci.ci_ind in
681		let mib = lookup_mind (fst ind) env.global_env in
	636	let mib = lookup_mind (fst ind) env.env in
682	637	let oib = mib.mind_packets.(snd ind) in
683	638	let () = check_compilable oib in
684	639	let rtbl = oib.mind_reloc_tbl in

715	670
716	671	\| Fix(rec_init,(names,type_bodies,rec_bodies)) ->
717	672	let ltypes = lambda_of_args env 0 type_bodies in
718		Renv.push_rels env names;
	673	let nenv = Renv.push_rec_types env (names, type_bodies, rec_bodies) in
	674	let lbodies = lambda_of_args nenv 0 rec_bodies in
	675	Lfix(rec_init, (names, ltypes, lbodies))
	676
	677	\| CoFix(init,(names,type_bodies,rec_bodies)) ->
	678	let ltypes = lambda_of_args env 0 type_bodies in
	679	let env = Renv.push_rec_types env (names, type_bodies, rec_bodies) in
	680	let map c ty = Reduction.eta_expand env.env c (Vars.lift (Array.length type_bodies) ty) in
	681	let rec_bodies = Array.map2 map rec_bodies type_bodies in
719	682	let lbodies = lambda_of_args env 0 rec_bodies in
720		Renv.popn env (Array.length names);
721		Lfix(rec_init, (names, ltypes, lbodies))
722
723		\| CoFix(init,(names,type_bodies,rec_bodies)) ->
724		let rec_bodies = Array.map2 (Reduction.eta_expand env.global_env) rec_bodies type_bodies in
725		let ltypes = lambda_of_args env 0 type_bodies in
726		Renv.push_rels env names;
727		let lbodies = lambda_of_args env 0 rec_bodies in
728		Renv.popn env (Array.length names);
729	683	Lcofix(init, (names, ltypes, lbodies))
730	684
731	685	\| Proj (p,c) ->

741	695	and lambda_of_app env f args =
742	696	match Constr.kind f with
743	697	\| Const (kn,u as c) ->
744		let kn = get_alias env.global_env kn in
745		let cb = lookup_constant kn env.global_env in
	698	let kn = get_alias env.env kn in
	699	let cb = lookup_constant kn env.env in
746	700	begin match cb.const_body with
747	701	\| Primitive op -> lambda_of_prim (kn,u) op (lambda_of_args env 0 args)
748	702	\| Def csubst when cb.const_inline_code ->

777	731
778	732	let lambda_of_constr ~optimize genv sigma c =
779	733	let env = Renv.make genv sigma in
780		let ids = List.rev_map Context.Rel.Declaration.get_annot (rel_context genv) in
781		Renv.push_rels env (Array.of_list ids);
782	734	let lam = lambda_of_constr env c in
783	735	let lam = if optimize then optimize_lambda lam else lam in
784	736	if !dump_lambda then

+3

-2

lib/spawn.ml less more

81	81	prerr_endline ("EXEC: " ^ String.concat " " (Array.to_list args));
82	82	let pid =
83	83	Unix.create_process_env prog args env Unix.stdin Unix.stdout Unix.stderr in
	84	prerr_endline ("PID " ^ string_of_int pid);
84	85	if pid = 0 then begin
85	86	Unix.sleep 1; (* to avoid respawning like crazy *)
86	87	raise (Failure "create_process failed")

179	180	close_out_noerr cout;
180	181	Option.iter close_in_noerr oob_resp;
181	182	Option.iter close_out_noerr oob_req;
182		if Sys.os_type = "Unix" then Unix.kill unixpid 9;
	183	if Sys.os_type = "Unix" then Unix.kill unixpid Sys.sigkill;
183	184	p.watch <- None
184	185	with e -> prerr_endline ("kill: "^Printexc.to_string e) end
185	186

249	250	close_out_noerr cout;
250	251	Option.iter close_in_noerr oob_resp;
251	252	Option.iter close_out_noerr oob_req;
252		if Sys.os_type = "Unix" then Unix.kill unixpid 9;
	253	if Sys.os_type = "Unix" then Unix.kill unixpid Sys.sigkill;
253	254	with e -> prerr_endline ("kill: "^Printexc.to_string e) end
254	255
255	256	let rec wait p =

+1

-1

tactics/rewrite.ml less more

297	297	let mk_relty evars newenv ty obj =
298	298	match obj with
299	299	\| None \| Some (_, None) ->
300		let evars, relty = mk_relation env evars ty in
	300	let evars, relty = mk_relation newenv evars ty in
301	301	if closed0 (goalevars evars) ty then
302	302	let env' = Environ.reset_with_named_context (Environ.named_context_val env) env in
303	303	new_cstr_evar evars env' relty

+7

-0

test-suite/bugs/bug_16645.v less more

	0	Goal False.
	1	Proof.
	2	assert (H: forall x:unit, False).
	3	{ native_cast_no_check (fun x:unit => I). }
	4	exact (H tt).
	5	Fail Qed.
	6	Abort.

+13

-0

test-suite/bugs/bug_16727.v less more

	0	Require Import Setoid.
	1
	2	Axiom R : unit -> unit -> Prop.
	3	Axiom RP : forall a b, R a b -> Prop.
	4
	5	Lemma RiemannInt_P2 :
	6	forall (a b: unit) (vn: R a b) (wn : R a a),
	7	RP a a wn ->
	8	{ l:unit \| True }.
	9	Proof.
	10	intros a b vn.
	11	try rewrite vn.
	12	Abort.

+12

-0

test-suite/bugs/bug_16752.v less more

	0	Axiom P : SProp.
	1	Axioms a b : P.
	2	Axiom Q : P->Prop.
	3	Axiom q : Q b.
	4	Axiom zog : forall p:P, Q p -> unit.
	5
	6	Lemma foobar : zog a q = tt.
	7	Proof.
	8	set (u := zog _ q).
	9	(* should be "u = tt" *)
	10	match goal with \|- u = tt => idtac end.
	11	Abort.

+85

-0

test-suite/bugs/bug_16829.v less more

	0	Require Import PrimInt63.
	1
	2	Open Scope uint63_scope.
	3
	4	Primitive array := #array_type.
	5
	6	Primitive make : forall A, int -> A -> array A := #array_make.
	7	Arguments make {_} _ _.
	8
	9	Primitive get : forall A, array A -> int -> A := #array_get.
	10	Arguments get {_} _ _.
	11
	12	Notation "t .[ i ]" := (get t i)
	13	(at level 2, left associativity, format "t .[ i ]").
	14
	15	Primitive set : forall A, array A -> int -> A -> array A := #array_set.
	16	Arguments set {_} _ _ _.
	17
	18	Notation "t .[ i <- a ]" := (set t i a)
	19	(at level 2, left associativity, format "t .[ i <- a ]").
	20
	21	Module Inconsistent.
	22	Definition P a := 0 = get (get a 1) 0.
	23	Definition H : P [\|[\|0\|0\|]; [\|0\|0\|] \|[\| \|0\|]\|] := eq_refl.
	24	Fail Definition bad : P (let m := [\| [\|0\|0\|]; [\|0\|0\|] \|[\| \|0\|]\|] in set (set m 0 (get m 0)) 1 [\| 1 \|0\|]) := H.
	25	(* Goal False. *)
	26	(* enough (eqb 1 0 = eqb 0 0) by (cbv in ; congruence). )
	27	(* rewrite bad; reflexivity. *)
	28	(* Qed. *)
	29
	30	Inductive CMP (x:array (unit -> nat)) := C.
	31
	32	Definition F (x:nat) := fun _:unit => x.
	33
	34	Definition TARGET := let m := [\| F 0; F 0 \| F 0 \|] in
	35	let m := set m 0 (fun _ => get (set m 1 (F 1)) 0 tt) in
	36	CMP m.
	37
	38	Definition EVALED := Eval cbv in TARGET.
	39
	40	Check C [\| F 0; F 0 \| F 0 \|] : EVALED.
	41	Check C [\| F 0; F 0 \| F 0 \|] <: EVALED.
	42	Check C [\| F 0; F 0 \| F 0 \|] <<: EVALED.
	43
	44	Fail Check C [\| F 0; F 1 \| F 0 \|] : TARGET.
	45	Fail Check C [\| F 0; F 1 \| F 0 \|] <: TARGET.
	46	Fail Check C [\| F 0; F 1 \| F 0 \|] <<: TARGET.
	47	End Inconsistent.
	48
	49	Module ShouldWork.
	50
	51	Definition mem := array (array int).
	52	Definition SCM := (mem -> mem) -> mem.
	53	Definition run : SCM -> mem := fun s => s (fun x => x).
	54	Definition ret : mem -> SCM := fun x k => k x.
	55	Definition bind : SCM -> (mem -> SCM) -> SCM := fun s f k => s (fun m => f m k).
	56
	57	Definition m := (make 2 (A:=array int) (make 0 (A:=int) 0))
	58	.[0 <- (make 2 (A:=int) 0).[0<-20] ]
	59	.[1 <- (make 2 (A:=int) 0).[0<-30].[1<-31] ].
	60
	61	Definition m_expected := (make 2 (A:=array int) (make 0 (A:=int) 0))
	62	.[0 <- (make 2 (A:=int) 0).[0<-200] ]
	63	.[1 <- (make 2 (A:=int) 0).[0<-30].[1<-300] ].
	64
	65	Definition assign_instr :=
	66	bind
	67	(bind (ret m) (fun m => ret (m.[0 <- m.[0].[0 <- 200]])))
	68	(fun m_inter => bind (ret m_inter) (fun m => ret (m.[1 <- m.[1].[1 <- 300]]))).
	69
	70	Lemma test2 : run assign_instr = m_expected.
	71	Proof.
	72	cbv. reflexivity.
	73	Qed.
	74
	75	End ShouldWork.
	76
	77	Definition bad_norm :=
	78	let m := make 2 (make 1 false) in
	79	m.[1 <- m.[1].[0 <- true]].[0 <- m.[0]].
	80
	81	Goal True.
	82	let x := eval lazy in bad_norm in
	83	constr_eq x [\| [\| false \| false : bool \|]; [\| true \| false : bool \|] \| [\| false \| false : bool \|] : array bool \|].
	84	Abort.

+16

-0

test-suite/bugs/bug_16831.v less more

	0	Set Primitive Projections.
	1	CoInductive Foo := B { p : bool }.
	2
	3	Definition f (x:=B false) (y:Foo) : Foo := cofix f := y.
	4
	5	Definition v := (f (B true)).(p).
	6
	7	Lemma v_true : v = true.
	8	Proof. reflexivity. Qed.
	9
	10	(* bad! *)
	11	Lemma v_false : v = false.
	12	Proof. vm_compute. Fail reflexivity. Abort.
	13
	14	Lemma v_false : v = false.
	15	Proof. native_compute. Fail reflexivity. Abort.

+6

-0

test-suite/output/bug_16411.out less more

	0	Axioms:
	1	foo : nat
	2	0
	3	: nat
	4	Axioms:
	5	axiom : nat

+9

-0

test-suite/output/bug_16411.v less more

	0	(* -- mode: coq; coq-prog-args: ("-vok") -- *)
	1
	2	Require Import TestSuite.for_vos.
	3
	4	Print Assumptions foo.
	5
	6	Check 0. (* separator *)
	7
	8	Print Assumptions bar.

+3

-0

test-suite/output/bug_16613.out less more

	0	File "./output/bug_16613.v", line 2, characters 2-10:
	1	Warning: This command does not support these attributes: bar, foo.
	2	[unsupported-attributes,parsing]

+2

-0

test-suite/output/bug_16613.v less more

	0	Set Warnings "unsupported-attributes".
	1	#[foo, bar] Definition foo := I.

+13

-0

test-suite/prerequisite/for_vos.v less more

	0	(* -- mode: coq; coq-prog-args: ("-vos") -- *)
	1
	2	Axiom axiom : nat.
	3
	4	Lemma foo : nat.
	5	Proof.
	6	exact axiom.
	7	Qed.
	8
	9	Lemma bar : nat.
	10	Proof.
	11	exact axiom.
	12	Defined.

+1

-0

test-suite/success/SchemeEquality.v less more

	0	(* -- coq-prog-args: ("-native-compiler" "no"); -- *)
0	1	(* Examples of use of Scheme Equality *)
1	2
2	3	Module A.

+1

-0

test-suite/success/extra_dep.v less more

7	7	From TestSuite Extra Dependency "extra_dep.txt" as d2.
8	8
9	9	Add LoadPath "prerequisite/subdir" as TestSuite.
	10	Set Warnings "+ambiguous-extra-dep".
10	11	Fail From TestSuite Extra Dependency "extra_dep.txt".
11	12	Fail Comments From TestSuite Extra Dependency "extra_dep.txt".

+3

-3

theories/Arith/Minus.v less more

52	52
53	53	#[deprecated(since="8.16",note="The Arith.Minus file is obsolete. Use Nat.add_sub_eq_l (and symmetry of equality) instead.")]
54	54	Notation plus_minus := Arith_prebase.plus_minus_stt.
55		#[deprecated(since="8.16",note="The Arith.Minus file is obsolete. Use Nat.add_sub (together with Nat.add_com) instead.")]
	55	#[deprecated(since="8.16",note="The Arith.Minus file is obsolete. Use Nat.add_sub (together with Nat.add_comm) instead.")]
56	56	Notation minus_plus := Arith_prebase.minus_plus_stt.
57		#[deprecated(since="8.16",note="The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_com) instead.")]
	57	#[deprecated(since="8.16",note="The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.")]
58	58	Notation le_plus_minus_r := Arith_prebase.le_plus_minus_r_stt.
59		#[deprecated(since="8.16",note="The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_com) instead.")]
	59	#[deprecated(since="8.16",note="The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.")]
60	60	Notation le_plus_minus := Arith_prebase.le_plus_minus_stt.
61	61
62	62	(** * Relation with order *)

+2

-2

tools/CoqMakefile.in less more

591	591	# There rules can be extended in @LOCAL_FILE@
592	592	# Extensions can't assume when they run.
593	593
	594	# findlib needs the package to not be installed, so we remove it before
	595	# installing it (see the call to findlib_remove)
594	596	install: META
595	597	$(HIDE)code=0; for f in $(FILESTOINSTALL); do\
596	598	if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \

605	607	echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\
606	608	fi;\
607	609	done
608		# findlib needs the package to not be installed, so we remove it before
609		# installing it
610	610	$(call findlib_remove)
611	611	$(call findlib_install, META $(FINDLIBFILESTOINSTALL))
612	612	$(HIDE)$(MAKE) install-extra -f "$(SELF)"

+2

-2

tools/configure/configure.ml less more

18	18
19	19	let (/) = Filename.concat
20	20
21		let coq_version = "8.16.0"
22		let vo_magic = 81600
	21	let coq_version = "8.16.1"
	22	let vo_magic = 81601
23	23	let is_a_released_version = true
24	24
25	25	(** Default OCaml binaries *)

+8

-8

tools/coqdep/common.ml less more

272	272
273	273	let findlib_resolve f package legacy_name plugin =
274	274	let open Fl_metascanner in
275		match find_META package, legacy_name with
276		\| None, Some p -> None, p
277		\| None, None -> Error.no_meta f package
278		\| Some (meta_file, meta), _ ->
	275	match find_META package with
	276	\| None -> Error.no_meta f package
	277	\| Some (meta_file, meta) ->
279	278	let rec find_plugin path p { pkg_defs ; pkg_children } =
280	279	match p with
281	280	\| [] -> path, pkg_defs

298	297	in
299	298	let path = [find_plugin_field "directory" (Some ".") meta.pkg_defs] in
300	299	let path, plug = find_plugin path plugin meta in
301		Some meta_file, String.concat "/" path ^ "/" ^
	300	meta_file, String.concat "/" path ^ "/" ^
302	301	Filename.chop_extension @@ find_plugin_field "plugin" None plug
303	302
304	303	let legacy_mapping = Core_plugins_findlib_compat.legacy_to_findlib

342	341	\| Declare sl ->
343	342	let public_to_private_name = function
344	343	\| [[x]] when List.mem_assoc x legacy_mapping ->
345		findlib_resolve f "coq-core" (Some x) (List.assoc x legacy_mapping)
	344	None, x
346	345	\| [[x]] ->
347	346	Error.findlib_name f x
348	347	\| [[legacy]; package :: plugin] ->
349		findlib_resolve f package (Some legacy) plugin
	348	None, legacy
350	349	\| [package :: plugin] ->
351		findlib_resolve f package None plugin
	350	let meta, cmxs = findlib_resolve f package None plugin in
	351	Some meta, cmxs
352	352	\| plist ->
353	353	CErrors.user_err
354	354	Pp.(str "Failed to resolve plugin " ++

+17

-7

vernac/assumptions.ml less more

220	220	let (curr, data, ax2ty) = accu in
221	221	let obj = ConstRef kn in
222	222	let already_in = GlobRef.Map_env.mem obj data in
223		let data = if not already_in then GlobRef.Map_env.add obj GlobRef.Set_env.empty data else data in
	223	let data = if not already_in then GlobRef.Map_env.add obj None data else data in
224	224	let ty = (current, ctx, Vars.subst1 mkProp oty) in
225	225	let ax2ty =
226	226	try let l = GlobRef.Map_env.find obj ax2ty in GlobRef.Map_env.add obj (ty::l) ax2ty

239	239	if already_in then data, ax2ty
240	240	else match body () (* Beware: this can be very costly *) with
241	241	\| None ->
242		GlobRef.Map_env.add obj GlobRef.Set_env.empty data, ax2ty
	242	GlobRef.Map_env.add obj None data, ax2ty
243	243	\| Some body ->
244	244	let contents,data,ax2ty =
245	245	traverse (label_of obj) Context.Rel.empty
246	246	(GlobRef.Set_env.empty,data,ax2ty) body in
247		GlobRef.Map_env.add obj contents data, ax2ty
	247	GlobRef.Map_env.add obj (Some contents) data, ax2ty
248	248	in
249	249	(GlobRef.Set_env.add obj curr, data, ax2ty)
250	250

293	293	let contents = GlobRef.Set_env.remove firstind_ref contents in
294	294	Array.fold_left_i (fun n data oib ->
295	295	let ind = (mind, n) in
296		let data = GlobRef.Map_env.add (GlobRef.IndRef ind) contents data in
	296	let data = GlobRef.Map_env.add (GlobRef.IndRef ind) (Some contents) data in
297	297	Array.fold_left_i (fun k data _ ->
298		GlobRef.Map_env.add (GlobRef.ConstructRef (ind, k+1)) contents data
	298	GlobRef.Map_env.add (GlobRef.ConstructRef (ind, k+1)) (Some contents) data
299	299	) data oib.mind_consnames) data mib.mind_packets
300	300	in
301	301	(data, ax2ty)

335	335	(* Only keep the transitive dependencies *)
336	336	let (_, graph, ax2ty) = traverse (label_of gr) t in
337	337	let open GlobRef in
338		let fold obj _ accu = match obj with
	338	let fold obj contents accu = match obj with
339	339	\| VarRef id ->
340	340	let decl = Global.lookup_named id in
341	341	if is_local_assum decl then

356	356	let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
357	357	ContextObjectMap.add (Axiom (TypeInType obj, l)) Constr.mkProp accu
358	358	in
359		if not (Declareops.constant_has_body cb) then
	359	if not (Option.has_some contents) then
360	360	let t = type_of_constant cb in
361	361	let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
362	362	ContextObjectMap.add (Axiom (Constant kn,l)) t accu

396	396	in
397	397	accu
398	398	in GlobRef.Map_env.fold fold graph ContextObjectMap.empty
	399
	400	(* Reexport a wrapper to preserve the 8.16 API *)
	401	let traverse current t =
	402	let (curr, graph, ax2ty) = traverse current t in
	403	let map = function
	404	\| None -> GlobRef.Set_env.empty
	405	\| Some s -> s
	406	in
	407	let graph = GlobRef.Map_env.map map graph in
	408	(curr, graph, ax2ty)

+1

-1

vernac/attributes.ml less more

40	40	let keys = List.map (fun x -> fst x.CAst.v) atts in
41	41	let keys = List.sort_uniq String.compare keys in
42	42	let conj = match keys with [_] -> "this attribute: " \| _ -> "these attributes: " in
43		Pp.(str "This command does not support " ++ str conj ++ prlist str keys ++ str"."))
	43	Pp.(str "This command does not support " ++ str conj ++ prlist_with_sep (fun () -> strbrk ", ") str keys ++ str"."))
44	44
45	45	let unsupported_attributes = function
46	46	\| [] -> ()

+2

-26

vernac/comExtraDeps.ml less more

10	10	open Names
11	11	open CErrors
12	12
13		let rec ensure_only_one_path_contains from file acc = function
14		\| [] ->
15		begin match acc with
16		\| Some x -> x
17		\| None ->
18		user_err Pp.(str "File " ++ str file ++ str " not found in " ++
19		DirPath.print from ++ str".")
20		end
21		\| x :: xs ->
22		let abspath = x ^ "/" ^ file in
23		if Sys.file_exists abspath then begin
24		match acc with
25		\| None -> ensure_only_one_path_contains from file (Some abspath) xs
26		\| Some other ->
27		user_err Pp.(str "File " ++ str file ++ str " found twice in " ++
28		DirPath.print from ++ str":" ++ spc () ++ str other ++ str "," ++
29		spc() ++ str abspath ++ str ".")
30		end else
31		ensure_only_one_path_contains from file acc xs
32
33	13	let extra_deps = Summary.ref ~name:"extra_deps" Id.Map.empty
34	14
35	15	let bind_extra_dep ?loc path id =

41	21	\| None -> extra_deps := Id.Map.add id (path,loc) !extra_deps
42	22
43	23	let declare_extra_dep ?loc ~from ~file id =
44		match Loadpath.find_with_logical_path from with
45		\| _ :: _ as paths ->
46		let paths = List.map Loadpath.physical paths in
47		let file_path = ensure_only_one_path_contains from file None paths in
48		Option.iter (bind_extra_dep ?loc file_path) id
49		\| [] -> user_err Pp.(str "No LoadPath found for " ++ DirPath.print from ++ str".")
	24	let file_path = Loadpath.find_extra_dep_with_logical_path ?loc ~from ~file () in
	25	Option.iter (bind_extra_dep ?loc file_path) id
50	26
51	27	let query_extra_dep id = fst @@ Id.Map.find id !extra_deps

+35

-0

vernac/loadpath.ml less more

46	46	(* get the list of load paths that correspond to a given logical path *)
47	47	let find_with_logical_path dirpath =
48	48	List.filter (fun p -> Names.DirPath.equal p.path_logical dirpath) !load_paths
	49
	50	let warn_file_found_multiple_times =
	51	CWarnings.create ~name:"ambiguous-extra-dep" ~category:"filesystem"
	52	(fun (file,from,other,extra) ->
	53	Pp.(str "File " ++ str file ++ str " found twice in " ++
	54	Names.DirPath.print from ++ str":" ++ spc () ++ str other ++ str " (selected)," ++
	55	spc() ++ str extra ++ str ".") )
	56
	57	let rec first_path_containing ?loc from file acc = function
	58	\| [] ->
	59	begin match acc with
	60	\| Some x -> x
	61	\| None ->
	62	CErrors.user_err Pp.(str "File " ++ str file ++ str " not found in " ++
	63	Names.DirPath.print from ++ str".")
	64	end
	65	\| x :: xs ->
	66	let abspath = x ^ "/" ^ file in
	67	if Sys.file_exists abspath then begin
	68	match acc with
	69	\| None -> first_path_containing ?loc from file (Some abspath) xs
	70	\| Some other ->
	71	warn_file_found_multiple_times ?loc (file,from,other,abspath);
	72	first_path_containing ?loc from file acc xs
	73	end else
	74	first_path_containing ?loc from file acc xs
	75
	76	let find_extra_dep_with_logical_path ?loc ~from ~file () =
	77	match find_with_logical_path from with
	78	\| _ :: _ as paths ->
	79	let paths = List.map physical paths in
	80	first_path_containing ?loc from file None paths
	81	\| [] -> CErrors.user_err
	82	Pp.(str "No LoadPath found for " ++ Names.DirPath.print from ++ str".")
	83
49	84
50	85	let remove_load_path dir =
51	86	let filter p = not (String.equal p.path_physical dir) in

+4

-0

vernac/loadpath.mli less more

42	42	val find_with_logical_path : Names.DirPath.t -> t list
43	43	(** get the list of load paths that correspond to a given logical path *)
44	44
	45	val find_extra_dep_with_logical_path :
	46	?loc:Loc.t -> from:Names.DirPath.t -> file:string -> unit -> CUnix.physical_path
	47	(** finds a file rooted in from. @raise UserError if the file is not found *)
	48
45	49	val locate_file : string -> string
46	50	(** Locate a file among the registered paths. Do not use this function, as
47	51	it does not respect the visibility of paths. *)

+2

-4

vernac/mltop.ml less more

71	71	(* We register errors at for Dynlink and Findlib, it is possible to
72	72	do so Symtable too, as we used to do in the bytecode init code.
73	73	*)
74		let _ = CErrors.register_handler (function
	74	let () = CErrors.register_handler (function
75	75	\| Dynlink.Error msg ->
76		let paths = Findlib.search_path () in
77		Some (hov 0 (str "Dynlink error: " ++ str (Dynlink.error_message msg) ++
78		cut () ++ str "Findlib paths:" ++ cut () ++ v 0 (prlist_with_sep cut str paths) ++ fnl()))
	76	Some (hov 0 (str "Dynlink error: " ++ str (Dynlink.error_message msg)))
79	77	\| Fl_package_base.No_such_package(p,msg) ->
80	78	let paths = Findlib.search_path () in
81	79	Some (hov 0 (str "Findlib error: " ++ str p ++