Execution Time of Array.pop

Stream: general

[Asei Inoue]

I expect the Array.pop function to run in constant time, but since the documentation comment does not mention its execution time, I'm not sure. Does Array.pop actually run in constant time?

[Asei Inoue]

In general, I believe it's a good habit to include the execution time in the documentation comment for functions marked with the @[extern] attribute.

[Patrick Stevens]

Implementation is https://github.com/leanprover/lean4/blob/7931e19572482f8a43ed11573d5c7e712ec9ddab/src/include/lean/lean.h#L872-L882 ; looks like if the array is used linearly then indeed it is constant time, while if it's non-exclusive then an array copy is incurred

[Wrenna Robson]

Are there any ways to enforce its use linearly?

[Asei Inoue]

I think so.” linear use linter” wanted.

[Henrik Böving]

This is a very difficult problem to solve in general, both at compile and even at run time for various reasons. There is much more than just a linter needed to solve this type of stuff.

[Asei Inoue]

partial linter would be also useful… which warns for clearly non-linear use