Changeset 2743 for extracted/PROBLEMS


Ignore:
Timestamp:
Feb 27, 2013, 9:27:58 PM (7 years ago)
Author:
sacerdot
Message:

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/PROBLEMS

    r2736 r2743  
    33================
    44
    5 1. ASM.subaddressing_modeel__o__mk_subaddressing_mode not extracted
    6   val subaddressing_modeel__o__mk_subaddressing_mode:
    7  Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector -> addressing_mode_tag Vector.vector -> addressing_mode -> addressing_mode
    8 
    9 2. File "monad.ml", line 1, characters 0-1:
    10 Error: The implementation monad.ml does not match the interface monad.cmi:
    11        Type declarations do not match:
    12          type monad0 = Preamble.__
    13        is not included in
    14          type 'a monad0
    15        They have different arities.
    16 
    17 Error: The implementation smallstepExec.ml
    18        does not match the interface smallstepExec.cmi:
    19        Type declarations do not match:
    20          type global = Preamble.__
    21        is not included in
    22          type ('a, 'b) global
    23        They have different arities.
     51. In some situations the types implemented with = __ in the .mli
     6   are less general than those in the .ml
    247
    258=========================
     
    2710=========================
    2811
    29 a) two in compiler.ml (the backend and the compiler itself)
    30    - file Fix.ml taken from the untrusted prototype and modified to
    31      redefine a few functions from OCaml's List due to module name shadowing
    32    - file compute_fixpoints.ml to adapt Fix.ml to the rest
    33 b) set_adt currently implemented by cut&paste from OCaml's set.ml, but
    34    using Pervasives.compare: the equality function taken in input is ignored!
     12In order to plug the untrusted code, the following files needs manual
     13intervention:
     14
     15a) compiler.ml
     16b) set_adt needs to be removed to favour the untrusted implementation
Note: See TracChangeset for help on using the changeset viewer.