[build] Build Coq without linkall

This PR is a draft to request for more comments, likely far from final
form yet.

See issue coq#9547

This is also related to PR coq#10951 and coq#7698

We seem to save half to one megabyte in the binaries:

```
-rwxr-xr-x 1 egallego egallego 31651662 janv. 31 00:05 coqc_bin.bc
-rwxr-xr-x 1 egallego egallego 32467231 janv. 31 00:08 coqc_bin.bc

-rwxr-xr-x 1 egallego egallego 23781840 janv. 31 00:05 coqc_bin.exe
-rwxr-xr-x 1 egallego egallego 24395352 janv. 31 00:08 coqc_bin.exe

-rwxr-xr-x 1 egallego egallego 23751520 janv. 31 00:05 coqtop_bin.exe
-rwxr-xr-x 1 egallego egallego 24395608 janv. 31 00:08 coqtop_bin.exe

-rwxr-xr-x 1 egallego egallego 41996191 janv. 31 00:05 coqtop_byte_bin.bc
-rwxr-xr-x 1 egallego egallego 43020328 janv. 31 00:08 coqtop_byte_bin.bc
```

Makefile.build

@@ -361,7 +361,7 @@ coqpp/coqpp_lex.cmo: coqpp/coqpp_ast.cmi coqpp/coqpp_parse.cmo
 
 $(COQPP): $(COQPPCMO) coqpp/coqpp_parser.mli coqpp/coqpp_parser.ml coqpp/coqpp_main.ml
 	$(SHOW)'OCAMLC -a $@'
-	$(HIDE)$(OCAMLC) -I coqpp $^ -linkall -o $@
+	$(HIDE)$(OCAMLC) -I coqpp $^ -o $@
 
 ###########################################################################
 # Specific rules for Uint63
@@ -388,15 +388,15 @@ $(COQC): $(COQCOPT:.opt=.$(BEST))
 
 bin/%.opt$(EXE): topbin/%_bin.ml $(LINKCMX) $(LIBCOQRUN)
 	$(SHOW)'COQMKTOP -o $@'
-	$(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) \
+	$(HIDE)$(OCAMLOPT) -linkpkg $(MLINCLUDES) \
 			   $(SYSMOD) \
 			   $(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@
 	$(STRIP_HIDE) $@
 	$(CODESIGN_HIDE) $@
 
 bin/%.byte$(EXE): topbin/%_bin.ml $(LINKCMO) $(LIBCOQRUN)
 	$(SHOW)'COQMKTOP -o $@'
-	$(HIDE)$(OCAMLC) -linkall -linkpkg $(MLINCLUDES) \
+	$(HIDE)$(OCAMLC) -linkpkg $(MLINCLUDES) \
 	                 -I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \
 			 $(SYSMOD) \
 			 $(LINKCMO) $(BYTEFLAGS) $< -o $@
@@ -407,7 +407,7 @@ COQTOP_BYTE=topbin/coqtop_byte_bin.ml
 # VMBYTEFLAGS will either contain -custom of the right -dllpath for the VM
 $(COQTOPBYTE): $(COQTOP_BYTE) $(LINKCMO) $(LIBCOQRUN)
 	$(SHOW)'COQMKTOP -o $@'
-	$(HIDE)$(OCAMLC) -linkall -linkpkg -I lib -I vernac -I toplevel \
+	$(HIDE)$(OCAMLC) -linkpkg -I lib -I vernac -I toplevel \
 	                 -I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \
 			 $(SYSMOD) -package compiler-libs.toplevel \
 			 $(LINKCMO) $(BYTEFLAGS) $< -o $@

Makefile.ide

@@ -152,15 +152,15 @@ $(IDETOPEXE): $(IDETOP:.opt=.$(BEST))
 
 $(IDETOP): ide/idetop.ml $(LINKCMX) $(LIBCOQRUN) $(IDETOPCMX)
 	$(SHOW)'COQMKTOP -o $@'
-	$(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) -I ide -I ide/protocol/ \
+	$(HIDE)$(OCAMLOPT) -linkpkg $(MLINCLUDES) -I ide -I ide/protocol/ \
 			   $(SYSMOD) \
 			   $(LINKCMX) $(IDETOPCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@
 	$(STRIP_HIDE) $@
 	$(CODESIGN_HIDE) $@
 
 $(IDETOPBYTE): ide/idetop.ml $(LINKCMO) $(LIBCOQRUN) $(IDETOPCMA)
 	$(SHOW)'COQMKTOP -o $@'
-	$(HIDE)$(OCAMLC) -linkall -linkpkg $(MLINCLUDES) -I ide -I ide/protocol/ \
+	$(HIDE)$(OCAMLC) -linkpkg $(MLINCLUDES) -I ide -I ide/protocol/ \
 	                 -I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \
 			 $(SYSMOD) \
 			 $(LINKCMO) $(IDETOPCMA) $(BYTEFLAGS) $< -o $@

ide/dune

@@ -21,8 +21,7 @@
  (package coqide-server)
  (modules idetop)
  (libraries coq.toplevel coqide-server.protocol)
- (modes native byte)
- (link_flags -linkall))
+ (modes native byte))
 
 (install
  (section bin)

plugins/funind/functional_principles_proofs.ml

@@ -1551,7 +1551,7 @@ let prove_principle_for_gen
         [
           Proofview.V82.of_tactic (generalize [lemma]);
           Proofview.V82.of_tactic (Simple.intro hid);
-          Proofview.V82.of_tactic (Elim.h_decompose_and (mkVar hid));
+          Proofview.V82.of_tactic (Ltac_plugin.Elim.h_decompose_and (mkVar hid));
           (fun g ->
              let new_hyps = pf_ids_of_hyps g in
              tcc_list := List.rev (List.subtract Id.equal new_hyps (hid::hyps));

plugins/funind/invfun.ml

@@ -93,7 +93,7 @@ let functional_inversion kn hid fconst f_correct = Proofview.Goal.enter (fun gl
       ; generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]
       ; clear [hid]
       ; Simple.intro hid
-      ; Inv.inv Inv.FullInversion None (Tactypes.NamedHyp hid)
+      ; Ltac_plugin.Inv.inv Ltac_plugin.Inv.FullInversion None (Tactypes.NamedHyp hid)
       ; Proofview.Goal.enter (fun gl ->
             let new_ids = List.filter (fun id -> not (Id.Set.mem id old_ids)) (pf_ids_of_hyps gl) in
             tclMAP (revert_graph kn pre_tac)  (hid::new_ids)

plugins/funind/recdef.ml

@@ -1300,7 +1300,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
             ; Proofview.Goal.enter (fun gl ->
                   let ids = pf_ids_of_hyps gl in
                   tclTHEN
-                    (Elim.h_decompose_and (mkVar hid))
+                    (Ltac_plugin.Elim.h_decompose_and (mkVar hid))
                     (Proofview.Goal.enter (fun gl ->
                          let ids' = pf_ids_of_hyps gl in
                          lid := List.rev (List.subtract Id.equal ids' ids);

tactics/autorewrite.ml → plugins/ltac/autorewrite.ml

@@ -288,4 +288,3 @@ let add_rew_rules base lrul =
         in incr counter;
           HintDN.add pat (!counter, rul) dn) HintDN.empty lrul
   in Lib.add_anonymous_leaf (inHintRewrite (base,lrul))
-

tactics/autorewrite.mli → plugins/ltac/autorewrite.mli

@@ -61,4 +61,3 @@ type hypinfo = {
 val find_applied_relation :
   ?loc:Loc.t -> bool ->
   Environ.env -> Evd.evar_map -> constr -> bool -> hypinfo
-

tactics/elim.ml → plugins/ltac/elim.ml

@@ -173,5 +173,3 @@ let double_ind h1 h2 =
   end
 
 let h_double_induction = double_ind
-
-

plugins/ltac/ltac_plugin.mlpack

@@ -1,3 +1,11 @@
+Dnet
+Elim
+Contradiction
+Inv
+Leminv
+Term_dnet
+Eqdecide
+Autorewrite
 Tacexpr
 Tacarg
 Tacsubst

plugins/omega/coq_omega.ml

@@ -28,7 +28,6 @@ open Tactics
 open Logic
 open Libnames
 open Nametab
-open Contradiction
 open Tactypes
 open Context.Named.Declaration
 
@@ -1112,7 +1111,7 @@ let replay_history tactic_normalisation =
                 unfold sp_Zle;
                 simpl_in_concl;
                 intro;
-                (absurd not_sup_sup) ])
+                (Ltac_plugin.Contradiction.absurd not_sup_sup) ])
               [ assumption ; reflexivity ]
           in
           let theorem =

tactics/tactics.mllib

@@ -2,7 +2,6 @@ DeclareScheme
 Declare
 Proof_global
 Pfedit
-Dnet
 Dn
 Btermdn
 Tacticals
@@ -16,15 +15,8 @@ Redexpr
 Ppred
 Tactics
 Abstract
-Elim
 Equality
-Contradiction
-Inv
-Leminv
 Hints
 Auto
 Eauto
 Class_tactics
-Term_dnet
-Eqdecide
-Autorewrite

topbin/dune

@@ -8,28 +8,25 @@
  (public_name coqtop.opt)
  (package coq)
  (modules coqtop_bin)
- (libraries coq.toplevel)
- (link_flags -linkall))
+ (libraries coq.toplevel))
 
 (executable
  (name coqtop_byte_bin)
  (public_name coqtop.byte)
  (package coq)
  (modules coqtop_byte_bin)
  (libraries compiler-libs.toplevel coq.toplevel)
- (modes byte)
- (link_flags -linkall))
+ (modes byte))
 
 (executable
  (name coqc_bin)
  (public_name coqc)
  (package coq)
  (modules coqc_bin)
  (libraries coq.toplevel)
- (modes native byte)
+ (modes native byte))
  ; Adding -ccopt -flto to links options could be interesting, however,
  ; it doesn't work on Windows
- (link_flags -linkall))
 
 (install
  (section bin)
@@ -42,8 +39,7 @@
  (public_names coqqueryworker.opt coqtacticworker.opt coqproofworker.opt)
  (package coq)
  (modules :standard \ coqtop_byte_bin coqtop_bin coqc_bin)
- (libraries coq.toplevel)
- (link_flags -linkall))
+ (libraries coq.toplevel))
 
 ; Workers installed targets
 (alias

user-contrib/Ltac2/tac2stdlib.ml

@@ -188,9 +188,9 @@ let to_strategy v = match Value.to_int v with
 let strategy = make_to_repr to_strategy
 
 let to_inversion_kind v = match Value.to_int v with
-| 0 -> Inv.SimpleInversion
-| 1 -> Inv.FullInversion
-| 2 -> Inv.FullInversionClear
+| 0 -> Ltac_plugin.Inv.SimpleInversion
+| 1 -> Ltac_plugin.Inv.FullInversion
+| 2 -> Ltac_plugin.Inv.FullInversionClear
 | _ -> assert false
 
 let inversion_kind = make_to_repr to_inversion_kind
@@ -534,7 +534,7 @@ let () = define_prim3 "tac_injection" bool (option intro_patterns) (option destr
 end
 
 let () = define_prim1 "tac_absurd" constr begin fun c ->
-  Contradiction.absurd c
+  Ltac_plugin.Contradiction.absurd c
 end
 
 let () = define_prim1 "tac_contradiction" (option constr_with_bindings) begin fun c ->

user-contrib/Ltac2/tac2tactics.ml

@@ -372,10 +372,10 @@ let autorewrite ~all by ids cl =
   let ids = List.map Id.to_string ids in
   let cl = mk_clause cl in
   match by with
-  | None -> Autorewrite.auto_multi_rewrite ?conds ids cl
+  | None -> Ltac_plugin.Autorewrite.auto_multi_rewrite ?conds ids cl
   | Some by ->
     let by = thaw Tac2ffi.unit by in
-    Autorewrite.auto_multi_rewrite_with ?conds by ids cl
+    Ltac_plugin.Autorewrite.auto_multi_rewrite_with ?conds by ids cl
 
 (** Auto *)
 
@@ -431,18 +431,18 @@ let inversion knd arg pat ids =
     begin match arg with
     | None -> assert false
     | Some (_, Tactics.ElimOnAnonHyp n) ->
-      Inv.inv_clause knd pat ids (AnonHyp n)
+      Ltac_plugin.Inv.inv_clause knd pat ids (AnonHyp n)
     | Some (_, Tactics.ElimOnIdent {CAst.v=id}) ->
-      Inv.inv_clause knd pat ids (NamedHyp id)
+      Ltac_plugin.Inv.inv_clause knd pat ids (NamedHyp id)
     | Some (_, Tactics.ElimOnConstr c) ->
       let open Tactypes in
       let anon = CAst.make @@ IntroNaming Namegen.IntroAnonymous in
       Tactics.specialize c (Some anon) >>= fun () ->
-      Tacticals.New.onLastHypId (fun id -> Inv.inv_clause knd pat ids (NamedHyp id))
+      Tacticals.New.onLastHypId (fun id -> Ltac_plugin.Inv.inv_clause knd pat ids (NamedHyp id))
     end
   in
   on_destruction_arg inversion true (Some (None, arg))
 
 let contradiction c =
   let c = Option.map mk_with_bindings c in
-  Contradiction.contradiction c
+  Ltac_plugin.Contradiction.contradiction c

user-contrib/Ltac2/tac2tactics.mli

@@ -119,6 +119,6 @@ val eauto : Hints.debug -> int option -> int option -> constr thunk list ->
 val typeclasses_eauto : Class_tactics.search_strategy option -> int option ->
   Id.t list option -> unit Proofview.tactic
 
-val inversion : Inv.inversion_kind -> destruction_arg -> intro_pattern option -> Id.t list option -> unit tactic
+val inversion : Ltac_plugin.Inv.inversion_kind -> destruction_arg -> intro_pattern option -> Id.t list option -> unit tactic
 
 val contradiction : constr_with_bindings option -> unit tactic

vernac/vernacstate.ml

@@ -8,6 +8,16 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+[@@@ocaml.warning "-60"]
+
+(* Link the proper modules *)
+module LinkMods = struct
+  let _ = G_prim.prim_kw
+  let _ = G_constr.constr_kw
+  let _ = G_proofs.thm_token
+  let _ = Himsg.explain_pretype_error
+end
+
 module Parser = struct
 
   type state = Pcoq.frozen_t