‏Terraform تو Lean 4: اگه کامپایل شد، احتمالاً دیپلوی هم می‌شه

نویسنده می‌گه دو آخرهفته وقت گذاشته و ابزاری به اسم infra ساخته: یه ابزار infrastructure-as-code (یعنی همون کاری که Terraform می‌کنه، منابع ابری رو با کد اعلام می‌کنی و ابزار اختلاف اون رو با وضعیت واقعی حساب‌های ابری برطرف می‌کنه) که با زبان Lean 4 نوشته شده. سه کلاد، ۱۴ نوع منبع، حدود ۱۵ هزار خط Lean و ۱۰۷ کامیت. صریح می‌گه نرم‌افزار پروداکشنی نیست و حرف اصلی مقاله اینه که یه سیستم تایپ واقعی به یه ابزار IaC چی اضافه می‌کنه.

fleet exampleQueue in paris where
  resource scaleway queues "infra-example"
    { visibilityTimeoutSec := 30 }

کل یه دیپلوی همینه. نکته‌ای که خودش هم انتظارش رو نداشته اینه: تو همین فایل in paris رو می‌شه با in warsaw عوض کرد و بازم کامپایل می‌شه، ولی تو فایل بغلی که هم‌زمان منابع AWS و Scaleway داره، in warsaw خطای کامپایله چون AWS تو ورشو منطقه‌ای نداره. یعنی مجاز بودن یه کلمه به بقیهٔ فایل بستگی داره.

به گفتهٔ نویسنده حلقهٔ کار همون حلقهٔ Terraform ـه (مشاهده، دیف، برطرف کردن اختلاف) و فرقش فقط جاییه که اشتباه‌ها گیر می‌افتن. ارجاع به منبعی که وجود نداره، فیلد اجباری جاافتاده، سرویسی که اون کلاد اصلاً نداره، سایز اینستنسی که وجود نداره و منطقه‌ای که کلاد توش نیست، همه سر کامپایل رد می‌شن. در عوض یکتا بودن اسم باکت و کوتا هنوز فقط موقع اجرا معلوم می‌شن، برای همین عنوان مقاله هم محتاطانه‌ست. مثلاً هر «مکان» جدا از کلاد تعریف شده و هر کلاد اونو به کد خودش نگاشت می‌کنه یا اصلاً نداره:

#guard Locality.paris.code .aws      = some "eu-west-3"
#guard Locality.paris.code .scaleway = some "fr-par"
#guard Locality.warsaw.code .aws     = none

نتیجه‌اش اینه که یه in paris هر دو کلاد رو درست جا می‌ده، کاری که با یه رشتهٔ region نمی‌شه کرد، و فهرست مکان‌های مجاز یه چیزیه که محاسبه می‌شه نه اینکه دستی نگه‌داری بشه؛ وقتی Scaleway میلان رو باز کرد، خودش به فهرست اضافه شد. سایز اینستنس هم رشته نیست: خانواده و سایز از دو مجموعهٔ بسته میان و کامپایلر همون جفت رو چک می‌کنه. رمزها (secret ها) هم نوعی دارن که خروجی JSON نداره و موقع چاپ redacted می‌شه، پس یه پسورد ثابت داخل فایل از چک رد نمی‌شه.

نویسنده منصفانه می‌گه فاصلهٔ مقیاس واقعیه: ۱۴ نوع منبع در برابر هزاران تای Terraform، سه کلاد در برابر صدها provider، بدون رجیستری ماژول و بدون state locking؛ اگه همین هفته باید زیرساخت بالا بیاری، سراغ Terraform برو. چیزی که به نظرش ارزش برداشتن به یه ابزار واقعی رو داره اینه: حالت مطلوب رو مقداری با نوع به‌قدر کافی تنگ بگیر تا نوشتن کانفیگ غیرقابل‌دیپلوی سخت شه، و چک‌های خودت رو بده کامپایلر اجرا کنه به‌جای نگه‌داری یه linter جدا که می‌تونه با تعریف واقعی فرق کنه.

نکات کلیدی:

• پروژه infra با Lean 4 نوشته شده: ۳ کلاد، ۱۴ نوع منبع، حدود ۱۵٬۰۰۰ خط، ۱۰۷ کامیت.
• جدول سایزها ۲۶ خانواده و ۱۷ سایز داره؛ ۲۵۷ ترکیب معتبر که کامپایلر چکشون می‌کنه.
• ارجاع بی‌مرجع ممکن نیست، چون نوع هر ارجاع کلاد و نوع منبع رو با خودش داره.
• شاخهٔ شرطی روی مقدار ناشناخته عمداً وجود نداره، پس برخلاف for_each در Terraform همیشه می‌شه plan ساخت.
• یکتایی نام باکت و کوتا هنوز خطای زمان اجرا هستن.
• Region.raw و InstanceType.raw راه فرار عمدی‌ان تا جدول قدیمی سد راه نشه.