!4#2792 Analysis.Normed.Field.Basic

Stream: mathlib4

[Jireh Loreaux]

@Scott Morrison this build failed during the library_search test file with an error I haven't seen before "timeout at delab". I have temporarily locally increased the maxHeartbeats to 300000. Would you mind having a look? I'm out of my depth here.

[Joël Riou]

I have had the same timeout issue while porting another (unrelated) file !4#2825

[Scott Morrison]

@Jireh Loreaux, @Joël Riou, merging master should resolve any such problems. The test file now has minimised imports.

[Jireh Loreaux]

!4#2792 now builds without issue and is ready for review (and hopefully merging)

[Ruben Van de Velde]

Oh, looks like it's in the queue already. Would you mind making a followup for my comments or should I?

[Jireh Loreaux]

I can

[Jireh Loreaux]

!4#2847, I'll change the port script in a separate PR

[Jireh Loreaux]

!4#2849 for the start_port.sh translations

[Ruben Van de Velde]

Thanks!