MSoegtropIMC

Require Import Ltac2.Ltac2.
Require Import Ltac2.Message.
Import Ltac2.Constr.Unsafe.
Require Ltac2.List.

Ltac2 rec message_indent (lvl:int) (m:message) :=
  match Int.equal lvl 0 with
  | true => m
  | false => concat (of_string " ") (message_indent (Int.sub lvl 1) m)
  end.

MSoegtropIMC

The attached files contain a piecwise degree 3 polynomial L-inf norm approximation for the sine and cosine function
in the interval 0...1 with 4 and 64 pieces.

The functions are sampled at the extrema of a Chebyshev polynomial of degree 4 since the residuals of an L-inf polynomial
approximation are by construction typically close to Chebyshev polynomials. The small deviations in the extrema positions usually
don't lead to substantial deviations in the extrema values.
This leads to rather small problems with only 5 variables (4 coefficients and one maximum error variable) and 10 inequalities
(5 extrema points, each positive and negative bounded).

The solution is implemented in:

MSoegtropIMC

From Mtac2 Require Import Mtac2 Ttactics.
Import TT.
Import TT.notations.


(*****************************************************************************)
(** * The sandbox I am playing in                                            *)
(*****************************************************************************)

Parameter A : Type.

MSoegtropIMC

(** * Tutorial for Mtac. *)
(**
    Author: Beta Ziliani
    
    Institution: Max Planck Institute for Software Systems (MPI-SWS)
*)

(* ToDo: a few upfront notes:

- I deliberately did not Import M, so that en explicit M. is required.

MSoegtropIMC

--- ./flexdll/cmdline.ml	2017-10-25 10:40:46.000000000 +0200
+++ ./flexdll/cmdline.ml	2019-02-19 21:41:18.157024900 +0100
@@ -248,6 +248,9 @@
         String.sub s 0 2 :: String.sub s 2 (String.length s - 2) :: tr rest
     | s :: rest when String.length s >= 5 && String.sub s 0 5 = "/link" ->
         "-link" :: String.sub s 5 (String.length s - 5) :: tr rest
+    (* Convert gcc linker option prefix -Wl, to flexlink linker prefix -link *)
+    | s :: rest when String.length s >= 6 && String.sub s 0 5 = "-Wl,-" ->
+        "-link" :: String.sub s 4 (String.length s - 4) :: tr rest
     | "-arg" :: x :: rest ->