[Agda] Agda options

[Ulf Norell]

On Wed, Mar 29, 2017 at 9:54 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

>
> 1.
> I use the option  -v profile:7
>
> Where the profiling option is referenced?
>

They're not, as far as I know. You can give -v profile.modules:10
or -v profile.definitions:10 to get a breakdown of the type checking
time per module or definition.

There's also -v profile.interactive:10 which will time Emacs mode commands
like C-c C-n.


> 2.
> The --help list shows the options  with-K, without-K.
> Which one is the default?
>

--with-K


> I have read certain explanation about the K axiom. It says that K means
> uniqueness of any identity proof.
> Suppose that one programs
>
>   f : (x y : Carrier) → x ≈ y → Carrier
>
> for any Setoid.  Does  with-K  option mean that the type checker
> presumes that it holds the property
>
>   (x y : Carrier) → x ≈ y → x ≡ y
> ?
>

No. Very much simplified, --without-K means you cannot pattern match
a proof of x ≡ x against refl.



> 3.
> I am trying to profile type checking on my application program.
> Agda type-checks many modules before coming to  Foo.agda.
> And  Foo.agda  has nothing besides importing modules and opening a
> certain parametric module with giving it a parameter instance.
>
> First all modules before  Foo.agda  are type-checked.
> Then I command
>
>   > agda $agdaLibOpt -v profile:7 +RTS -K90m -M8G -RTS  Foo.agda
>
> And it reports
>
> ------------------------------------------------------------------
> Loading M1
> Loading M2
> ...
> Loading  FactorizationRing.FtRing
> (/home/mechvel/agda/tosave/bugs/tcPerf-mar28-2017/
> FactorizationRing/FtRing.agdai).
>
> Finished Foo.
> Total                        143,264ms
> Miscellaneous                    300ms
> Serialization                 67,128ms (75,508ms)
> Serialization.BuildInterface   4,648ms
> Serialization.BinaryEncode     3,148ms
> Serialization.Sort               332ms
> Serialization.Compress           252ms
> Deserialization               51,819ms
> DeadCode                       8,212ms
> Typing                         7,296ms
> Scoping                           64ms     (84ms)
> Scoping.InverseScopeLookup        20ms
> Import                            44ms
> -------------------------------------------------------------------
>
> "Loading  FactorizationRing.FtRing"
> means that this module is only being loaded but not type-checked.
> Right?
>

Yes.


> About  Foo.agda,  it does not report Loading nor "checking".
> And I expect that the time segment between the report of
> "Loading  FactorizationRing.FtRing"  and before appearing of
> "Finished Foo"  is the time taken by type-checking  Foo.agda.
> Right?
>

Right. It does say "Checking Foo" at the top. It loads the other modules
as it finds the import statements during scope checking, so there
might be some scope checking time before the last "Loading", but
no type checking.


> 3.1.
> The `time' command shows that this process lasts about  144 sec.
>
> So, I guess that in the line
>                         "Total       143,264ms"
>
> comma parts thousands, so that this means 143 seconds and 264
> milliseconds.
> Right?
>

Yes.


>
> 3.2.
> What is Serialization and Deserialization (in short) ?
> What does it mean the second number (in parentheses) in the line of
> Serialization?
>

Serialization is the writing of interface files for type checked modules and
Deserialization is the reading of such interface files (the 'Loading' bit).
The number in parenthesis is including all subentries
(Serialization.BuildInterfaces, ...).


> Having the above profiling, how can we derive the time spent to
> "Loading" ready modules before starting to type-check Foo.agda ?
> (I observe that it is about 50 seconds).
>

Deserialization               51,819ms

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170330/2adf2186/attachment-0001.html>