16Mb memory limit

[leodemoura]

When I try to process Jakob's file on the web, I get the following error message:

 -- Processing file ...
Cannot enlarge memory arrays. Either (1) compile with -s TOTAL_MEMORY=X with X higher than the current value 16777216, (2) compile with ALLOW_MEMORY_GROWTH which adjusts the size at runtime but prevents some optimizations, or (3) set Module.TOTAL_MEMORY before the program runs.
 -- Saved to 'Dropbox/Apps/Lean.JS/input.lean'.

Here is his file

import hott.path
open path function

-- Equivalences
-- ------------

definition Sect {A B : Type} (s : A → B) (r : B → A) := Πx : A, r (s x) ≈ x

-- -- TODO: need better means of declaring structures
-- -- TODO: note that Coq allows projections to be declared to be coercions on the fly

-- Structure IsEquiv

inductive IsEquiv [class] {A B : Type} (f : A → B) :=
IsEquiv_mk : Π
  (inv : B → A)
  (retr : Sect inv f)
  (sect : Sect f inv)
  (adj : Πx, retr (f x) ≈ ap f (sect x)),
IsEquiv f

namespace IsEquiv

  definition inv {A B : Type} {f : A → B} (H : IsEquiv f) : B → A :=
    IsEquiv.rec (λinv retr sect adj, inv) H

  -- TODO: note: does not type check without giving the type
  definition retr {A B : Type} {f : A → B} (H : IsEquiv f) : Sect (inv H) f :=
    IsEquiv.rec (λinv retr sect adj, retr) H

  definition sect {A B : Type} {f : A → B} (H : IsEquiv f) : Sect f (inv H) :=
    IsEquiv.rec (λinv retr sect adj, sect) H

  definition adj {A B : Type} {f : A → B} (H : IsEquiv f) :
         Πx, retr H (f x) ≈ ap f (sect H x) :=
    IsEquiv.rec (λinv retr sect adj, adj) H

end IsEquiv

-- Structure Equiv

inductive Equiv (A B : Type) : Type :=
Equiv_mk : Π
  (equiv_fun : A → B)
  (equiv_isequiv : IsEquiv equiv_fun),
Equiv A B

namespace Equiv

  definition equiv_fun [coercion] {A B : Type} (e : Equiv A B) : A → B :=
    Equiv.rec (λequiv_fun equiv_isequiv, equiv_fun) e

  definition equiv_isequiv [coercion] {A B : Type} (e : Equiv A B) : IsEquiv (equiv_fun e) :=
    Equiv.rec (λequiv_fun equiv_isequiv, equiv_isequiv) e

  infix `≃`:25 := Equiv
  notation e `⁻¹` := IsEquiv.inv e

end Equiv

  -- Some instances and closure properties of equivalences

namespace IsEquiv
  variables {A B C : Type} {f : A → B} {g : B → C} {f' : A → B}

  -- The identity function is an equivalence.

  definition idIsEquiv [instance] : (@IsEquiv A A id) := IsEquiv_mk id (λa, idp) (λa, idp) (λa, idp)

  -- The composition of two equivalences is, again, an equivalence.

  definition comp_closed [instance] (Hf : IsEquiv f) (Hg : IsEquiv g) : (IsEquiv (g ∘ f)) :=
    IsEquiv_mk ((inv Hf) ∘ (inv Hg))
           (λc, ap g (retr Hf ((inv Hg) c)) @ retr Hg c)
           (λa, ap (inv Hf) (sect Hg (f a)) @ sect Hf a)
           (λa, (whiskerL _ (adj Hg (f a))) @
            (ap_pp g _ _)^ @
            ap02 g (concat_A1p (retr Hf) (sect Hg (f a))^ @
                (ap_compose (inv Hf) f _ @@ adj Hf a) @
                (ap_pp f _ _)^
               ) @
            (ap_compose f g _)^
           )

  -- Any function equal to an equivalence is an equivlance as well.
  definition path_closed (Hf : IsEquiv f) (Heq : f ≈ f') : (IsEquiv f') :=
     path.induction_on Heq Hf

  -- Any function pointwise equal to an equivalence is an equivalence as well.
  definition sim_closed (Hf : IsEquiv f) (Heq : f ∼ f') : (IsEquiv f') :=
    let sect' := (λ b, (Heq (inv Hf b))^ @ retr Hf b) in
    let retr' := (λ a, (ap (inv Hf) (Heq a))^ @ sect Hf a) in
    let adj' := (λ (a : A),
      let ff'a := Heq a in
      let invf := inv Hf in
      let secta := sect Hf a in
      let retrfa := retr Hf (f a) in
      let retrf'a := retr Hf (f' a) in
      have eq1 : ap f secta @ ff'a ≈ ap f (ap invf ff'a) @ retr Hf (f' a),
        from calc ap f secta @ ff'a
              ≈ retrfa @ ff'a : (ap _ (adj Hf _ ))^
          ... ≈ ap (λb, f (invf b)) ff'a @ retrf'a : (!concat_A1p)^
          ... ≈ ap f (ap invf ff'a) @ retr Hf (f' a) : {ap_compose invf f ff'a},
      have eq2 : retrf'a ≈ Heq (invf (f' a)) @ ((ap f' (ap invf ff'a))^ @ ap f' secta),
        from calc retrf'a
              ≈ (ap f (ap invf ff'a))^ @ (ap f secta @ ff'a) :(moveL_Vp _ _ _ (eq1^))
          ... ≈ ap f (ap invf ff'a)^ @ (ap f secta @ Heq a) : {ap_V invf ff'a}
          ... ≈ ap f (ap invf ff'a)^ @ (Heq (invf (f a)) @ ap f' secta) : {!concat_Ap}
          ... ≈ ap f (ap invf ff'a)^ @ Heq (invf (f a)) @ ap f' secta : {!concat_pp_p^}
          ... ≈ ap f ((ap invf ff'a)^) @ Heq (invf (f a)) @ ap f' secta : {!ap_V^}
          ... ≈ Heq (invf (f' a)) @ ap f' ((ap invf ff'a)^) @ ap f' secta : {!concat_Ap}
          ... ≈ Heq (invf (f' a)) @ (ap f' (ap invf ff'a))^ @ ap f' secta : {!ap_V}
          ... ≈ Heq (invf (f' a)) @ ((ap f' (ap invf ff'a))^ @ ap f' secta) : !concat_pp_p,
      have eq3 : (Heq (invf (f' a)))^ @ retr Hf (f' a) ≈ ap f' ((ap invf ff'a)^ @ secta),
        from calc (Heq (invf (f' a)))^ @ retr Hf (f' a)
              ≈ (ap f' (ap invf ff'a))^ @ ap f' secta : moveR_Vp _ _ _ eq2
          ... ≈ (ap f' ((ap invf ff'a)^)) @ ap f' secta : {!ap_V^}
          ... ≈ ap f' ((ap invf ff'a)^ @ secta) : (!ap_pp)^,
    eq3) in
  IsEquiv_mk (inv Hf) sect' retr' adj'

  --TODO: Maybe wait until rewrite rules are available.
  theorem inv_closed (Hf : IsEquiv f) : (IsEquiv (inv Hf)) :=
    IsEquiv_mk sorry sorry sorry sorry

end IsEquiv

namespace Equiv

  variables {A B C : Type} (eqf : A ≃ B)

  theorem id : A ≃ A := Equiv_mk id IsEquiv.idIsEquiv

  theorem compose (eqg: B ≃ C) : A ≃ C :=
    Equiv_mk ((equiv_fun eqg) ∘ (equiv_fun eqf))
         (IsEquiv.comp_closed (equiv_isequiv eqf) (equiv_isequiv eqg))

  check IsEquiv.path_closed

  theorem path_closed (f' : A → B) (Heq : equiv_fun eqf ≈ f') : A ≃ B :=
    Equiv_mk f' (IsEquiv.path_closed (equiv_isequiv eqf) Heq)

  theorem inv_closed : B ≃ A :=
    Equiv_mk (IsEquiv.inv (equiv_isequiv eqf)) (IsEquiv.inv_closed (equiv_isequiv eqf))

end Equiv

[soonhokong]

Hi @leodemoura ,

I've added a URL option mem. Please try: http://www.cs.cmu.edu/~soonhok/lean.js/?mem=32 It will run lean.js with 32MB memory. On my machine, it process Jakob's file in 3 seconds without memory error.

Later, we will add a "settings" icon where we can customize many options.

[leodemoura]

I tried it and it didn't work for me. I still get the error

 -- Processing file ...
Cannot enlarge memory arrays. Either (1) compile with -s TOTAL_MEMORY=X with X higher than the current value 16777216, (2) compile with ALLOW_MEMORY_GROWTH which adjusts the size at runtime but prevents some optimizations, or (3) set Module.TOTAL_MEMORY before the program runs.
 -- Failed to write to 'Dropbox/Apps/Lean.JS/input.lean'.

Do I have to flush the cache?

[leodemoura]

On my machine, it process Jakob's file in 3 seconds without memory error.

It seems the js version is 10x slower than the native one. It takes 0.3secs to process his file using native lean.

[leodemoura]

It is working now. I don't know why. I closed/opened chrome, and it didn't work. I tried again with ?mem=64, and it worked. Then, I tried again with ?mem=32 and it worked ?!?!?

[soonhokong]

For the record, I guess what happened is that the web-browser cached js/main.js and used the old one. As a result, it didn't pick up the newly introduced option mem.