From 2836860cd4b31f98db1de3cf494de22110976284 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 27 Feb 2026 15:06:38 +0100 Subject: [PATCH 1/6] Fix handling of configure time VM disabling --- sysinit/coqargs.ml | 16 +++++++++++----- sysinit/coqargs.mli | 1 + sysinit/coqinit.ml | 6 ++++++ .../Corelib/Numbers/Cyclic/Int63/Sint63Axioms.v | 2 +- .../Corelib/Numbers/Cyclic/Int63/Uint63Axioms.v | 2 +- 5 files changed, 20 insertions(+), 7 deletions(-) diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml index 141e6cec5ecf..cfdbe0cf6161 100644 --- a/sysinit/coqargs.ml +++ b/sysinit/coqargs.ml @@ -41,6 +41,7 @@ type require_injection = { lib: string; prefix: string option; export: export_fl type injection_command = | OptionInjection of (string list * option_command) | RequireInjection of require_injection + | WarnNoBytecode | WarnNoNative of string | WarnNativeDeprecated @@ -106,8 +107,6 @@ type t = { let default_toplevel = "Top" -let default_native = Coq_config.native_compiler - let default_logic_config = { impredicative_set = false; indices_matter = false; @@ -120,8 +119,8 @@ let default_config = { logic = default_logic_config; rcfile = None; coqlib = None; - enable_VM = true; - native_compiler = default_native; + enable_VM = Coq_config.bytecode_compiler; + native_compiler = Coq_config.native_compiler; native_output_dir = ".coq-native"; native_include_dirs = []; output_directory = None; @@ -229,6 +228,10 @@ let parse_option_set opt = let v = String.sub opt (eqi+1) (len - eqi - 1) in to_opt_key (String.sub opt 0 eqi), Some v +let get_bytecode_compiler_warns b = + if b && not Coq_config.bytecode_compiler then [WarnNoBytecode] + else [] + let get_native_compiler s = (* We use two boolean flags because the four states make sense, even if only three are accessible to the user at the moment. The selection of the @@ -345,7 +348,10 @@ let parse_args ~init arglist : t * string list = |"-w" | "-W" -> add_set_warnings oval (next()) |"-bytecode-compiler" -> - { oval with config = { oval.config with enable_VM = get_bool ~opt (next ()) }} + let b = get_bool ~opt (next ()) in + let warn = get_bytecode_compiler_warns b in + { oval with config = { oval.config with enable_VM = b }; + pre = { oval.pre with injections = warn @ oval.pre.injections }} |"-native-compiler" -> let native_compiler, warn = get_native_compiler (next ()) in diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli index fa04c49c55be..2c5436f04c2f 100644 --- a/sysinit/coqargs.mli +++ b/sysinit/coqargs.mli @@ -30,6 +30,7 @@ type injection_command = | RequireInjection of require_injection (** Require libraries before the initial state is ready. *) + | WarnNoBytecode | WarnNoNative of string (** Used so that "-w -native-compiler-disabled -native-compiler yes" does not cause a warning. The native option must be processed diff --git a/sysinit/coqinit.ml b/sysinit/coqinit.ml index a588d88b1067..d6f777fbb8de 100644 --- a/sysinit/coqinit.ml +++ b/sysinit/coqinit.ml @@ -219,6 +219,11 @@ let require_file ~intern ~prefix ~lib ~export ~allow_failure = with (Synterp.UnmappedLibrary _ | Synterp.NotFoundLibrary _) when allow_failure -> warn_require_not_found (mfrom, mp) +let warn_no_bytecode = + CWarnings.create ~name:"bytecode-compiler-disabled" ~category:CWarnings.CoreCategories.bytecode_compiler + Pp.(fun () -> str "Bytecode compiler is disabled," ++ spc() ++ + str "-bytecode-compiler option ignored.") + let warn_no_native_compiler = CWarnings.create_in Nativeconv.w_native_disabled Pp.(fun s -> strbrk "Native compiler is disabled," ++ @@ -253,6 +258,7 @@ let handle_injection ~intern = let open Coqargs in function | RequireInjection {lib;prefix;export;allow_failure} -> require_file ~intern ~lib ~prefix ~export ~allow_failure | OptionInjection o -> set_option o + | WarnNoBytecode -> warn_no_bytecode () | WarnNoNative s -> warn_no_native_compiler s | WarnNativeDeprecated -> warn_deprecated_native_compiler () diff --git a/theories/Corelib/Numbers/Cyclic/Int63/Sint63Axioms.v b/theories/Corelib/Numbers/Cyclic/Int63/Sint63Axioms.v index 297b4640c0fc..0ad8ea8daee8 100644 --- a/theories/Corelib/Numbers/Cyclic/Int63/Sint63Axioms.v +++ b/theories/Corelib/Numbers/Cyclic/Int63/Sint63Axioms.v @@ -20,7 +20,7 @@ Local Infix "^" := Z.pow : Z_scope. Local Notation "x <= y" := (Z.compare x y <> Gt) : Z_scope. Local Notation "x < y" := (Z.compare x y = Lt) : Z_scope. -Definition min_int := Eval vm_compute in (lsl 1 62). +Definition min_int := Eval lazy in (lsl 1 62). (** Translation to and from Z *) Definition to_Z (i : int) := diff --git a/theories/Corelib/Numbers/Cyclic/Int63/Uint63Axioms.v b/theories/Corelib/Numbers/Cyclic/Int63/Uint63Axioms.v index ba73c75c5a20..5b05142a16a9 100644 --- a/theories/Corelib/Numbers/Cyclic/Int63/Uint63Axioms.v +++ b/theories/Corelib/Numbers/Cyclic/Int63/Uint63Axioms.v @@ -32,7 +32,7 @@ Definition size := 63%nat. Definition digits := 63%uint63. (** The biggest int *) -Definition max_int := Eval vm_compute in sub 0 1. +Definition max_int := Eval lazy in sub 0 1. (** Access to the nth digits *) Definition get_digit x p := ltb 0 (land x (lsl 1 p)). From 2a90093fb510d0b46fa6e909c8aeffbc5bc02563 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 2 Mar 2026 14:49:17 +0100 Subject: [PATCH 2/6] Checker warn if given -bytecode-compiler and VM configured off --- checker/coqchk_main.ml | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/checker/coqchk_main.ml b/checker/coqchk_main.ml index 8ec2cf428ad2..cc288948a20b 100644 --- a/checker/coqchk_main.ml +++ b/checker/coqchk_main.ml @@ -146,11 +146,22 @@ let indices_matter = ref false let enable_vm = ref false +let warn_no_bytecode = + CWarnings.create ~name:"bytecode-compiler-disabled" ~category:CWarnings.CoreCategories.bytecode_compiler + Pp.(fun () -> + str "Bytecode compiler is disabled," ++ spc() ++ + str "-bytecode-compiler option ignored.") + let make_senv () = let senv = Safe_typing.empty_environment in let senv = Safe_typing.set_impredicative_set !impredicative_set senv in let senv = Safe_typing.set_indices_matter !indices_matter senv in - let senv = Safe_typing.set_VM !enable_vm senv in + let senv = + if !enable_vm && not Coq_config.bytecode_compiler then begin + warn_no_bytecode (); + senv + end else Safe_typing.set_VM !enable_vm senv + in let senv = Safe_typing.set_allow_sprop true senv in (* be smarter later *) Safe_typing.set_native_compiler false senv From 5972e4abe62b1cad6cbffed8003d06893ad22b7a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 27 Feb 2026 15:11:20 +0100 Subject: [PATCH 3/6] More robust handling of env typing flags wrt configure VM/native disabling --- kernel/declareops.ml | 8 ++++++-- kernel/environ.ml | 7 +++++++ 2 files changed, 13 insertions(+), 2 deletions(-) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 7dab6c0dca99..7d2898650175 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -19,6 +19,10 @@ let noh hcons x = snd (hcons x) (** Operations concernings types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) +let configure_enabled_native = match Coq_config.native_compiler with + | NativeOff -> false + | NativeOn _ -> true + let safe_flags oracle = { check_guarded = true; check_positive = true; @@ -27,8 +31,8 @@ let safe_flags oracle = { conv_oracle = oracle; share_reduction = true; unfold_dep_heuristic = false; - enable_VM = true; - enable_native_compiler = true; + enable_VM = Coq_config.bytecode_compiler; + enable_native_compiler = configure_enabled_native; indices_matter = true; impredicative_set = false; sprop_allowed = true; diff --git a/kernel/environ.ml b/kernel/environ.ml index 65cd4df5fed2..67be9e5848d6 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -598,11 +598,18 @@ let same_flags { allow_uip == alt.allow_uip [@warning "+9"] +let check_flags c = + assert (Coq_config.bytecode_compiler || not c.enable_VM); + assert (match Coq_config.native_compiler with + | NativeOff -> not c.enable_native_compiler + | NativeOn _ -> true) + let set_type_in_type b = map_universes (UGraph.set_type_in_type b) let set_typing_flags c env = if same_flags env.env_typing_flags c then env else + let () = check_flags c in let env = { env with env_typing_flags = c } in let env = set_type_in_type (not c.check_universes) env in let env = { env with env_qualities = QGraph.set_ignore_constraints (not c.check_eliminations) env.env_qualities } in From 48ad2148d8ad5905b5f27142c12ced3f9d416f00 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 27 Feb 2026 15:11:54 +0100 Subject: [PATCH 4/6] Vmbytegen.compile return None if VM disabled --- kernel/vmbytegen.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml index cef33cd6a45a..f4b05057234b 100644 --- a/kernel/vmbytegen.ml +++ b/kernel/vmbytegen.ml @@ -975,6 +975,7 @@ let warn_compile_error = Vmerrors.pr_error let compile ~fail_on_error ~uinstance env sigma c = + if not (typing_flags env).enable_VM then None else try NewProfile.profile "vm_compile" (fun () -> Some (compile ~uinstance env sigma c)) () with Vmerrors.CompileError msg as exn -> let exn = Exninfo.capture exn in From b0649ccfcaaf124b68e993985807bc8fc6be6624 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 27 Feb 2026 15:21:00 +0100 Subject: [PATCH 5/6] Lazy conversion add flag to disable first order approximation, use for VM fallback --- kernel/conversion.ml | 23 +++++++++++++++++++---- kernel/conversion.mli | 10 ++++++++-- kernel/mod_typing.ml | 4 ++-- kernel/subtyping.ml | 2 +- kernel/typeops.ml | 2 +- kernel/vconv.ml | 4 ++-- pretyping/reductionops.ml | 10 +++++----- pretyping/reductionops.mli | 2 +- 8 files changed, 39 insertions(+), 18 deletions(-) diff --git a/kernel/conversion.ml b/kernel/conversion.ml index aa4c0bd3a1a4..4e7ee7623bcb 100644 --- a/kernel/conversion.ml +++ b/kernel/conversion.ml @@ -119,6 +119,11 @@ let pure_stack lfts stk = (* Conversion *) (********************************************************************) +type firstorder_mode = + | Eager + | L2R + | R2L + (* Conversion utility functions *) (* functions of this type are called from the kernel *) @@ -126,7 +131,7 @@ type 'a kernel_conversion_function = env -> 'a -> 'a -> (unit, unit) result (* functions of this type can be called from outside the kernel *) type 'a extended_conversion_function = - ?l2r:bool -> ?reds:TransparentState.t -> env -> + ?l2r:firstorder_mode -> ?reds:TransparentState.t -> env -> ?evars:evar_handler -> 'a -> 'a -> (unit, unit) result @@ -384,7 +389,12 @@ let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv = and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = Control.check_for_interrupt (); (* First head reduce both terms *) - let ninfos = infos_with_reds infos.cnv_inf RedFlags.betaiotazeta in + let ninfos = match l2r with + | Eager -> + let all = RedFlags.(red_add_transparent all (red_transparent (info_flags infos.cnv_inf))) in + infos_with_reds infos.cnv_inf all + | L2R | R2L -> infos_with_reds infos.cnv_inf RedFlags.betaiotazeta + in let appr1 = whd_stack ninfos infos.lft_tab (fst st1) (snd st1) in let appr2 = whd_stack ninfos infos.rgt_tab (fst st2) (snd st2) in eqwhnf cv_pb l2r infos (lft1, appr1) (lft2, appr2) cuniv @@ -466,6 +476,11 @@ and eqwhnf cv_pb l2r infos (lft1, (hd1, v1) as appr1) (lft2, (hd2, v2) as appr2) let () = Control.check_for_interrupt () in (* Determine which constant to unfold first *) let unfold_left = + let l2r = match l2r with + | L2R -> true + | R2L -> false + | Eager -> assert false + in let order = Conv_oracle.oracle_compare oracle (to_er fl1) (to_er fl2) in match order with | Conv_oracle.Left -> true @@ -1014,7 +1029,7 @@ let () = let state = info_univs infos in let qual_equal q1 q2 = CClosure.eq_quality infos q1 q2 in let infos = { cnv_inf = infos; cnv_typ = true; lft_tab = tab; rgt_tab = tab; err_ret = box; } in - let state', _ = ccnv CONV false infos el_id el_id a b (state, checked_universes_gen qual_equal) in + let state', _ = ccnv CONV R2L infos el_id el_id a b (state, checked_universes_gen qual_equal) in assert (state==state'); true with @@ -1023,7 +1038,7 @@ let () = in CClosure.set_conv conv -let gen_conv ~typed cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=default_evar_handler env) t1 t2 = +let gen_conv ~typed cv_pb ?(l2r=R2L) ?(reds=TransparentState.full) env ?(evars=default_evar_handler env) t1 t2 = let univs = Environ.universes env in let state = univs in let b = diff --git a/kernel/conversion.mli b/kernel/conversion.mli index d42217f8e0f5..1a2fd22b5b2c 100644 --- a/kernel/conversion.mli +++ b/kernel/conversion.mli @@ -14,9 +14,15 @@ open Environ (*********************************************************************** s conversion functions *) +(** Which side to unfold first (default: R2L ie unfold right side first) *) +type firstorder_mode = + | Eager + | L2R + | R2L + type 'a kernel_conversion_function = env -> 'a -> 'a -> (unit, unit) result type 'a extended_conversion_function = - ?l2r:bool -> ?reds:TransparentState.t -> env -> + ?l2r:firstorder_mode -> ?reds:TransparentState.t -> env -> ?evars:CClosure.evar_handler -> 'a -> 'a -> (unit, unit) result @@ -57,7 +63,7 @@ val conv_leq : types extended_conversion_function (** The failure values depend on the universe state functions (for better error messages). *) -val generic_conv : conv_pb -> l2r:bool +val generic_conv : conv_pb -> l2r:firstorder_mode -> TransparentState.t -> env -> ?evars:CClosure.evar_handler -> ('a, 'err) generic_conversion_function diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index f136f31f5dfc..e40a1b06b59c 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -53,10 +53,10 @@ let rec rebuild_mp mp l = | i::r -> rebuild_mp (MPdot(mp,i)) r let infer_gen_conv state env c1 c2 = - Conversion.generic_conv Conversion.CONV ~l2r:false TransparentState.full env state c1 c2 + Conversion.generic_conv Conversion.CONV ~l2r:R2L TransparentState.full env state c1 c2 let infer_gen_conv_leq state env c1 c2 = - Conversion.generic_conv Conversion.CUMUL ~l2r:false TransparentState.full env state c1 c2 + Conversion.generic_conv Conversion.CUMUL ~l2r:R2L TransparentState.full env state c1 c2 type with_body = { w_def : Constr.t; diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 15e9fb67c71e..f12bcf5e43e8 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -89,7 +89,7 @@ let check_conv_error error why state poly pb env a1 a2 = if poly then match Conversion.default_conv pb env a1 a2 with | Result.Ok () -> fst state | Result.Error () -> error (IncompatiblePolymorphism (env, a1, a2)) - else match Conversion.generic_conv pb ~l2r:false TransparentState.full env state a1 a2 with + else match Conversion.generic_conv pb ~l2r:R2L TransparentState.full env state a1 a2 with | Result.Ok state -> state | Result.Error None -> error why | Result.Error (Some (Univ e)) -> error (IncompatibleUniverses { err = e; env; t1 = a1; t2 = a2 }) diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 2f837f7afbb9..f62d01aa5b1e 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -528,7 +528,7 @@ let should_invert_case env r ci = let type_case_scrutinee env (mib, _mip) (u', largs) u pms (pctx, p) c = let (params, realargs) = List.chop mib.mind_nparams largs in (* Check that the type of the scrutinee is <= the expected argument type *) - let iter p1 p2 = match Conversion.conv ~l2r:true env p1 p2 with + let iter p1 p2 = match Conversion.conv ~l2r:L2R env p1 p2 with | Result.Ok () -> () | Result.Error () -> raise NotConvertible in diff --git a/kernel/vconv.ml b/kernel/vconv.ml index d675d352a8f2..5ff300b090ca 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -220,7 +220,7 @@ let warn_bytecode_compiler_failed = let vm_conv_gen (type err) cv_pb sigma env univs t1 t2 = if not (typing_flags env).Declarations.enable_VM then - Conversion.generic_conv cv_pb ~l2r:false ~evars:sigma.Genlambda.evars_val + Conversion.generic_conv cv_pb ~l2r:Eager ~evars:sigma.Genlambda.evars_val TransparentState.full env univs t1 t2 else let exception Error of err in @@ -235,7 +235,7 @@ let vm_conv_gen (type err) cv_pb sigma env univs t1 t2 = | Error e -> Result.Error (Some e) | Not_found | Invalid_argument _ | Vmerrors.CompileError _ -> warn_bytecode_compiler_failed (); - Conversion.generic_conv cv_pb ~l2r:false ~evars:sigma.Genlambda.evars_val + Conversion.generic_conv cv_pb ~l2r:Eager ~evars:sigma.Genlambda.evars_val TransparentState.full env univs t1 t2 let vm_conv cv_pb env t1 t2 = diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 1730bb25e60e..4ce079eb20a7 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1253,7 +1253,7 @@ let is_fconv ?(reds=TransparentState.full) pb env sigma t1 t2 = let evars = Evd.evar_handler sigma in try let env = Environ.set_universes (Evd.universes sigma) env in - begin match Conversion.generic_conv ~l2r:false pb ~evars reds env (sigma, CheckUnivs.checked_universes) t1 t2 with + begin match Conversion.generic_conv ~l2r:R2L pb ~evars reds env (sigma, CheckUnivs.checked_universes) t1 t2 with | Result.Ok (_ : Evd.evar_map) -> true | Result.Error None -> false | Result.Error (Some e) -> Empty.abort e @@ -1282,7 +1282,7 @@ let is_conv_nounivs ?(reds=TransparentState.full) env sigma t1 t2 = compare_cumul_instances = (fun _ _ _ _ () -> Ok ()); } in - begin match Conversion.generic_conv ~l2r:false CONV ~evars reds env ((), ignore_univs) t1 t2 with + begin match Conversion.generic_conv ~l2r:R2L CONV ~evars reds env ((), ignore_univs) t1 t2 with | Result.Ok () -> true | Result.Error None -> false | Result.Error (Some e) -> Empty.abort e @@ -1341,7 +1341,7 @@ let univproblem_univ_state = compare_cumul_instances = univproblem_check_inductive_instances; } type genconv = { - genconv : 'a 'err. conv_pb -> l2r:bool -> Evd.evar_map -> TransparentState.t -> + genconv : 'a 'err. conv_pb -> l2r:Conversion.firstorder_mode -> Evd.evar_map -> TransparentState.t -> Environ.env -> ('a, 'err) Conversion.generic_conversion_function } @@ -1371,7 +1371,7 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Conversion.CUMUL) approximation. This may result in unsatisfiable constraints even if some unfoldings of the arguments could have been unified, but this should be exceedingly rare. *) - let ans = match conv_fun.genconv pb ~l2r:false sigma ts env (UnivProblem.Set.empty, univproblem_univ_state) x y with + let ans = match conv_fun.genconv pb ~l2r:R2L sigma ts env (UnivProblem.Set.empty, univproblem_univ_state) x y with | Result.Ok cstr -> Some cstr | Result.Error None -> None (* no universe unification can make these terms convertible *) @@ -1384,7 +1384,7 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Conversion.CUMUL) | sigma -> Some sigma | exception UGraph.UniverseInconsistency _ | exception Evd.UniversesDiffer -> (* Retry with local universe checking, which may imply constant unfolding *) - match conv_fun.genconv pb ~l2r:false sigma ts env (sigma, sigma_univ_state) x y with + match conv_fun.genconv pb ~l2r:R2L sigma ts env (sigma, sigma_univ_state) x y with | Result.Ok sigma -> Some sigma | Result.Error None -> None | Result.Error (Some e) -> raise (UGraph.UniverseInconsistency e) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index f003559812f0..0634fe47bec3 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -273,7 +273,7 @@ val native_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr -> evar_map option type genconv = { - genconv : 'a 'err. conv_pb -> l2r:bool -> Evd.evar_map -> TransparentState.t -> + genconv : 'a 'err. conv_pb -> l2r:Conversion.firstorder_mode -> Evd.evar_map -> TransparentState.t -> Environ.env -> ('a, 'err) Conversion.generic_conversion_function } From d0b7d16378d99bff3d314b67251f80a1c05b4367 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 2 Mar 2026 14:50:36 +0100 Subject: [PATCH 6/6] Refman disable vm-compute-disabled warning --- doc/tools/rocqrst/repl/rocqtop.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/tools/rocqrst/repl/rocqtop.py b/doc/tools/rocqrst/repl/rocqtop.py index 0ce28ec24cd3..24c27f299ac2 100644 --- a/doc/tools/rocqrst/repl/rocqtop.py +++ b/doc/tools/rocqrst/repl/rocqtop.py @@ -103,7 +103,7 @@ def sendone(self, sentence): def send_initial_options(self): """Options to send when starting the toplevel and after a Reset Initial.""" self.sendone('Set Rocqtop Exit On Error.') - self.sendone('Set Warnings "+default".') + self.sendone('Set Warnings "+default,-vm-compute-disabled".') def sendmany(*sentences): """A small demo: send each sentence in sentences and print the output"""