diff options
| -rw-r--r-- | Makefile.build | 3 | ||||
| -rw-r--r-- | checker/checker.ml | 1 | ||||
| -rw-r--r-- | configure.ml | 2 | ||||
| -rw-r--r-- | dev/doc/build-system.dune.md | 4 | ||||
| -rw-r--r-- | dev/shim/dune | 13 | ||||
| -rw-r--r-- | dune | 2 | ||||
| -rw-r--r-- | kernel/cPrimitives.ml | 2 | ||||
| -rw-r--r-- | kernel/mod_subst.ml | 3 | ||||
| -rw-r--r-- | kernel/primred.ml | 4 | ||||
| -rw-r--r-- | kernel/retroknowledge.ml | 1 | ||||
| -rw-r--r-- | kernel/retroknowledge.mli | 1 | ||||
| -rw-r--r-- | kernel/type_errors.ml | 5 | ||||
| -rw-r--r-- | kernel/type_errors.mli | 3 | ||||
| -rw-r--r-- | kernel/typeops.ml | 21 | ||||
| -rw-r--r-- | tools/coq_dune.ml | 7 | ||||
| -rw-r--r-- | vernac/himsg.ml | 18 |
16 files changed, 62 insertions, 28 deletions
diff --git a/Makefile.build b/Makefile.build index 8b989f161a..2e4700be88 100644 --- a/Makefile.build +++ b/Makefile.build @@ -620,6 +620,9 @@ gramlib/.pack/gramlib.cmxa: $(GRAMOBJS:.cmo=.cmx) gramlib/.pack/gramlib.cmx $(SHOW)'OCAMLOPT -a -o $@' $(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -a -o $@ $^ +# used by install +gramlib/.pack/gramlib_MLLIB_DEPENDENCIES:=$(GRAMFILES) + # Specific rule for kernel.cma, with $(VMBYTEFLAGS). # This helps loading dllcoqrun.so during an ocamldebug kernel/kernel.cma: kernel/kernel.mllib diff --git a/checker/checker.ml b/checker/checker.ml index 3c93ef7d36..d3f346d76b 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -273,6 +273,7 @@ let explain_exn = function | IllFormedBranch _ -> str"IllFormedBranch" | Generalization _ -> str"Generalization" | ActualType _ -> str"ActualType" + | IncorrectPrimitive _ -> str"IncorrectPrimitive" | CantApplyBadType ((n,a,b),{uj_val = hd; uj_type = hdty},args) -> let pp_arg i judge = hv 1 (str"arg " ++ int (i+1) ++ str"= " ++ diff --git a/configure.ml b/configure.ml index ef38651a4d..8b6fccb5e3 100644 --- a/configure.ml +++ b/configure.ml @@ -1101,7 +1101,7 @@ let write_configml f = pr_b "native_compiler" !prefs.nativecompiler; let core_src_dirs = [ "config"; "lib"; "clib"; "kernel"; "library"; - "engine"; "pretyping"; "interp"; "gramlib/.pack"; "parsing"; "proofs"; + "engine"; "pretyping"; "interp"; "gramlib"; "gramlib/.pack"; "parsing"; "proofs"; "tactics"; "toplevel"; "printing"; "ide"; "stm"; "vernac" ] in let core_src_dirs = List.fold_left (fun acc core_src_subdir -> acc ^ " \"" ^ core_src_subdir ^ "\";\n") "" diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index a31ab1c511..b1bfac8cc9 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -126,9 +126,9 @@ script again] This will be fixed in the future. ## Dropping from coqtop: -The following sequence is recommended: +After doing `make -f Makefile.dune voboot`, the following commands should work: ``` -dune exec coqtop.byte +dune exec dev/shim/coqbyte-prelude > Drop. # #directory "dev";; # #use "include_dune";; diff --git a/dev/shim/dune b/dev/shim/dune index 85a0d205da..39b4ef492c 100644 --- a/dev/shim/dune +++ b/dev/shim/dune @@ -11,6 +11,19 @@ (run chmod +x %{targets}))))) (rule + (targets coqbyte-prelude) + (deps + %{bin:coqtop.byte} + %{lib:coq.kernel:../../stublibs/dllbyterun_stubs.so} + %{project_root}/theories/Init/Prelude.vo) + (action + (with-outputs-to %{targets} + (progn + (echo "#!/usr/bin/env bash\n") + (bash "echo \"$(pwd)/%{bin:coqtop.byte} -coqlib $(pwd)/%{project_root}\" \"$@\"") + (run chmod +x %{targets}))))) + +(rule (targets coqide-prelude) (deps %{bin:coqqueryworker.opt} @@ -19,7 +19,7 @@ (deps (source_tree theories) (source_tree plugins)) - (action (with-stdout-to .vfiles.d (bash "%{bin:coqdep} -dyndep opt -noglob -boot `find theories plugins -type f -name *.v`")))) + (action (with-stdout-to .vfiles.d (bash "%{bin:coqdep} -dyndep both -noglob -boot `find theories plugins -type f -name *.v`")))) (alias (name vodeps) diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml index da5c4fb07b..fdc93cfa89 100644 --- a/kernel/cPrimitives.ml +++ b/kernel/cPrimitives.ml @@ -148,7 +148,7 @@ let prim_ind_to_string = function | PIT_cmp -> "cmp" let prim_type_to_string = function - | PT_int63 -> "int63" + | PT_int63 -> "int63_type" let op_or_type_to_string = function | OT_op op -> to_string op diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index cd675653cb..9397772415 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -339,9 +339,6 @@ let subst_retro_action subst action = | Register_type(prim,c) -> let c' = subst_constant subst c in if c == c' then action else Register_type(prim, c') - | Register_inline(c) -> - let c' = subst_constant subst c in - if c == c' then action else Register_inline(c') (* Here the semantics is completely unclear. What does "Hint Unfold t" means when "t" is a parameter? diff --git a/kernel/primred.ml b/kernel/primred.ml index d95d7de7aa..d6d0a6143a 100644 --- a/kernel/primred.ml +++ b/kernel/primred.ml @@ -44,10 +44,6 @@ let add_retroknowledge env action = { retro with retro_cmp = Some r } in set_retroknowledge env retro - | Register_inline(c) -> - let (cb,r) = lookup_constant_key c env in - let cb = {cb with Declarations.const_inline_code = true} in - add_constant_key c cb !(fst r) env let get_int_type env = match env.retroknowledge.retro_int63 with diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index 18fafdb6d3..e1c4cec5b5 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -38,4 +38,3 @@ let empty = { type action = | Register_ind of CPrimitives.prim_ind * inductive | Register_type of CPrimitives.prim_type * Constant.t - | Register_inline of Constant.t diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 1554fe88da..09e8140308 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -25,4 +25,3 @@ val empty : retroknowledge type action = | Register_ind of CPrimitives.prim_ind * inductive | Register_type of CPrimitives.prim_type * Constant.t - | Register_inline of Constant.t diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 964d32c6b3..481ffc290c 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -55,6 +55,7 @@ type ('constr, 'types) ptype_error = | IllFormedBranch of 'constr * pconstructor * 'constr * 'constr | Generalization of (Name.t * 'types) * ('constr, 'types) punsafe_judgment | ActualType of ('constr, 'types) punsafe_judgment * 'types + | IncorrectPrimitive of (CPrimitives.op_or_type,'types) punsafe_judgment * 'types | CantApplyBadType of (int * 'constr * 'constr) * ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array | CantApplyNonFunctional of ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array @@ -120,6 +121,9 @@ let error_generalization env nvar c = let error_actual_type env j expty = raise (TypeError (env, ActualType (j,expty))) +let error_incorrect_primitive env p t = + raise (TypeError (env, IncorrectPrimitive (p, t))) + let error_cant_apply_not_functional env rator randl = raise (TypeError (env, CantApplyNonFunctional (rator,randl))) @@ -175,6 +179,7 @@ let map_ptype_error f = function | IllFormedBranch (c, pc, t1, t2) -> IllFormedBranch (f c, pc, f t1, f t2) | Generalization ((na, t), j) -> Generalization ((na, f t), on_judgment f j) | ActualType (j, t) -> ActualType (on_judgment f j, f t) +| IncorrectPrimitive (p, t) -> IncorrectPrimitive ({p with uj_type=f p.uj_type}, f t) | CantApplyBadType ((n, c1, c2), j, vj) -> CantApplyBadType ((n, f c1, f c2), on_judgment f j, Array.map (on_judgment f) vj) | CantApplyNonFunctional (j, jv) -> CantApplyNonFunctional (on_judgment f j, Array.map (on_judgment f) jv) diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 4b832930e1..c5ab9a4e73 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -56,6 +56,7 @@ type ('constr, 'types) ptype_error = | IllFormedBranch of 'constr * pconstructor * 'constr * 'constr | Generalization of (Name.t * 'types) * ('constr, 'types) punsafe_judgment | ActualType of ('constr, 'types) punsafe_judgment * 'types + | IncorrectPrimitive of (CPrimitives.op_or_type,'types) punsafe_judgment * 'types | CantApplyBadType of (int * 'constr * 'constr) * ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array | CantApplyNonFunctional of ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array @@ -112,6 +113,8 @@ val error_generalization : env -> Name.t * types -> unsafe_judgment -> 'a val error_actual_type : env -> unsafe_judgment -> types -> 'a +val error_incorrect_primitive : env -> (CPrimitives.op_or_type,types) punsafe_judgment -> types -> 'a + val error_cant_apply_not_functional : env -> unsafe_judgment -> unsafe_judgment array -> 'a diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 7eb8e803b3..227a164549 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -252,6 +252,11 @@ let type_of_prim env t = in nary_int63_op (CPrimitives.arity t) return_ty +let type_of_prim_or_type env = let open CPrimitives in + function + | OT_type t -> type_of_prim_type env t + | OT_op op -> type_of_prim env op + let judge_of_int env i = make_judge (Constr.mkInt i) (type_of_int env) @@ -664,17 +669,7 @@ let judge_of_case env ci pj cj lfj = (* Building type of primitive operators and type *) -open CPrimitives - let check_primitive_type env op_t t = - match op_t with - | OT_type PT_int63 -> - (try - default_conv ~l2r:false CUMUL env mkSet t - with NotConvertible -> - CErrors.user_err Pp.(str"Was expecting the sort of this primitive type to be Set")) - | OT_op p -> - (try - default_conv ~l2r:false CUMUL env (type_of_prim env p) t - with NotConvertible -> - CErrors.user_err Pp.(str"Not the expected type for this primitive")) + let inft = type_of_prim_or_type env op_t in + try default_conv ~l2r:false CUMUL env inft t + with NotConvertible -> error_incorrect_primitive env (make_judge op_t inft) t diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml index 62a871aa0e..98368d76ca 100644 --- a/tools/coq_dune.ml +++ b/tools/coq_dune.ml @@ -235,6 +235,12 @@ let scan_plugins m = let dirs = Sys.(List.filter (fun f -> is_plugin_directory @@ bpath ["plugins";f]) Array.(to_list @@ readdir "plugins")) in List.fold_left scan_mlg m dirs +(* This will be removed when we drop support for Make *) +let fix_cmo_cma file = + if String.equal Filename.(extension file) ".cmo" + then replace_ext ~file ~newext:".cma" + else file + (* Process .vfiles.d and generate a skeleton for the dune file *) let parse_coqdep_line l = match Str.(split (regexp ":") l) with @@ -249,6 +255,7 @@ let parse_coqdep_line l = the platform. Anyways, I hope we can link to coqdep instead of having to parse its output soon, that should solve this kind of issues *) + let deps = List.map fix_cmo_cma deps in Some (String.split_on_char '/' dir, VO { target; deps; }) (* Otherwise a vio file, we ignore *) | _ -> None diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 9e92d936d2..2ef2317d86 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -339,6 +339,20 @@ let explain_actual_type env sigma j t reason = str "while it is expected to have type" ++ brk(1,1) ++ pt ++ ppreason ++ str ".") +let explain_incorrect_primitive env sigma j exp = + let env = make_all_name_different env sigma in + let {uj_val=p;uj_type=t} = j in + let t = Reductionops.nf_betaiota env sigma t in + let exp = Reductionops.nf_betaiota env sigma exp in + (* Actually print *) + let pe = pr_ne_context_of (str "In environment") env sigma in + let (pt, pct) = pr_explicit env sigma exp t in + pe ++ + hov 0 ( + str "The primitive" ++ brk(1,1) ++ str (CPrimitives.op_or_type_to_string p) ++ spc () ++ + str "has type" ++ brk(1,1) ++ pct ++ spc () ++ + str "while it is expected to have type" ++ brk(1,1) ++ pt ++ str ".") + let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl = let randl = jv_nf_betaiotaevar env sigma randl in let actualtyp = Reductionops.nf_betaiota env sigma actualtyp in @@ -720,7 +734,9 @@ let explain_type_error env sigma err = | Generalization (nvar, c) -> explain_generalization env sigma nvar c | ActualType (j, pt) -> - explain_actual_type env sigma j pt None + explain_actual_type env sigma j pt None + | IncorrectPrimitive (j, t) -> + explain_incorrect_primitive env sigma j t | CantApplyBadType (t, rator, randl) -> explain_cant_apply_bad_type env sigma t rator randl | CantApplyNonFunctional (rator, randl) -> |