اوپن میتھ ہارنس کیا ہے؟
اوپن میتھ ہارنس، اوپن میتھ OS کے پسِ پردہ اوپن سورس رن ٹائم ہے۔ اس کی پہلی نسل، جس کا نام Nucleus ہے، Rust میں لکھی گئی ہے اور اس میں پلیٹ فارم کے زیرِ استعمال کرنل، سروسز اور ایجنٹس شامل ہیں۔
یہ رن ٹائم باہمی تعاون پر مبنی ریاضیاتی تحقیق کے لیے تیار کیا گیا ہے۔ یہ اوپن ویٹ ماڈلز پر چلنے والے ایجنٹس، Ultramath کے ذریعے متوازی مسئلہ جاتی تحقیق، Lean سے تصدیق شدہ ثبوت کی تلاش، پروجیکٹ میموری، ٹولز اور محفوظ کارروائیوں کے لیے انسانی منظوری فراہم کر سکتا ہے۔
موجودہ پابندی: مکمل رن ٹائم کا انحصار Open Math OS کے تعیناتی ماحول پر ہے۔ ریپوزٹری کو سورس سے بنایا جا سکتا ہے اور اس میں ایک چھوٹی خود کفیل مثال شامل ہے، لیکن یہ ابھی تک انٹرایکٹو ایجنٹس، Ultramath، میموری یا ثبوت کی تلاش کے لیے الگ سے چلنے والا مقامی ماحول فراہم نہیں کرتی۔
بنیادی ڈیزائن اور خصوصیات
صلاحیتوں پر مبنی پابندی
اوپن میتھ ہارنس صلاحیتوں پر مبنی مائیکروکرنل استعمال کرتا ہے۔ ہر پراسیس کو صرف وہی اختیار ملتا ہے جو اس کی تشکیل کے ذریعے دیا گیا ہو، اور اس کے ذریعے شروع کیا جانے والا کوئی بھی پراسیس والد پراسیس کی جانب سے تفویض کیے جانے والے اختیار سے زیادہ اختیار حاصل نہیں کرتا۔ یہ اصول ایجنٹس اور دیگر پروگراموں دونوں پر لاگو ہوتا ہے۔
ماڈل کے جوابات، ٹول کے نتائج، ریپوزٹری کی فائلیں اور دیگر متن غیر معتبر اِن پٹ تصور کیے جاتے ہیں۔ متن اجازتیں نہیں دے سکتا، محفوظ کارروائیوں کی منظوری نہیں دے سکتا اور یہ طے نہیں کر سکتا کہ کوئی ثبوت درست ہے یا نہیں۔ اسناد محدود اختیارات رکھنے والے فراہم کنندگان میں رہتی ہیں، انہیں ماڈلز، ٹرانسکرپٹس یا لاگز کے سامنے ظاہر نہیں کیا جاتا۔
ایجنٹس اور تحقیقی ٹولز
- اوپن ماڈل ایجنٹس: سیشنز اوپن ویٹ ماڈلز کو اسٹریمنگ جوابات، ٹولز، ذیلی ایجنٹس اور مستقل تاریخ کے ساتھ استعمال کر سکتے ہیں۔
- Ultramath: متعدد ایجنٹس کسی مشکل مسئلے کے مختلف طریقوں کی غیر ہم وقت تحقیق کرتے ہیں، نتائج کا اشتراک کرتے ہیں اور ایک رابطہ کار ایجنٹ کو رپورٹس بھیجتے ہیں۔
- ثبوت کی تلاش: ورکرز ممکنہ Lean ثبوتوں کے درخت میں شاخوں کی تحقیق کرتے ہیں۔ کوئی امیدوار صرف اسی صورت کامیاب ہوتا ہے جب Lean اصل بیان کے مقابلے میں اس کی تصدیق کرے۔
- پروجیکٹ ٹولز: ایجنٹس ریپوزٹری کی فائلوں، شیل، ویب اور PDF ٹولز، پروجیکٹ اسکلز، MCP سرورز اور پلگ اِنز کے ساتھ کام کر سکتے ہیں۔
- انسانی کنٹرول: محفوظ کارروائیاں منظوری تک رکی رہتی ہیں، جبکہ سیشن ریکارڈز کو دکھانے سے پہلے رازوں کے لیے اسکین کیا جاتا ہے۔
پروجیکٹ میموری
میموری ہر پروجیکٹ کے لیے الگ برقرار رکھی جاتی ہے۔ جب کوئی سیشن پُرسکون ہو جائے تو میموری سروس اس کی تاریخ سے مفید مواد اخذ کر سکتی ہے اور منتخب معلومات کو MEMORY.md میں یکجا کر سکتی ہے۔ بعد کے سیشنز اس میموری کو سیاق و سباق کے طور پر حاصل کرتے ہیں اور استعمال کیے گئے مواد کا حوالہ دیتے ہیں۔
میموری صرف سیاق و سباق فراہم کرتی ہے۔ یہ اجازتیں نہیں دے سکتی اور نہ ہی صارف کی موجودہ ہدایات کو نظرانداز کر سکتی ہے۔
ضروریات
اوپن میتھ ہارنس بنانے سے پہلے درج ذیل انحصارات کے ساتھ ایک معاونت یافتہ Linux ماحول تیار کریں:
- Linux: Windows اور macOS کو مقامی رن ٹائم ہوسٹس کے طور پر سپورٹ نہیں کیا جاتا۔
- مقامی بلڈ ٹولز: مقامی انحصارات کے لیے C کمپائلر اور لنکر انسٹال کریں۔
- rustup کے ذریعے Rust: ریپوزٹری کی
rust-toolchain.tomlمطلوبہ ٹول چین کو مقرر کرتی ہے اور فارمیٹنگ اور linting کے اجزا شامل کرتی ہے۔ - bubblewrap:
bwrapانسٹال کریں، اسےPATHمیں شامل کریں اور یقینی بنائیں کہ ہوسٹ غیر مراعات یافتہ صارف نیم اسپیسز کی اجازت دیتا ہے۔
پابندی لازمی ہے۔ اگر bubblewrap ہوسٹ کی سیکیورٹی پالیسی کے باعث اپنا سینڈ باکس نہیں بنا سکتا تو رن ٹائم آغاز کے دوران ناکام ہو جائے گا۔
اوپن میتھ ہارنس کو سورس سے بنائیں
ریپوزٹری کلون کریں، اس کی ڈائریکٹری میں جائیں اور مکمل Rust ورک اسپیس بنائیں:
git clone https://github.com/openmathmodel/open-math-harness.git
cd open-math-harness
cargo build --locked --workspace--locked آپشن Cargo کو لاک فائل میں درج انحصاری ورژنز استعمال کرنے پر مجبور کرتا ہے۔ کامیاب بلڈ کے بعد لانچر اور سروس بائنریز target/debug/ کے اندر دستیاب ہوں گی۔
deploy/vm/کے اندر موجود فائلیں منظم Open Math OS ورچوئل مشین کے لیے ہیں۔ یہ ذاتی کمپیوٹر کے لیے الگ سے چلنے والا انسٹالر نہیں ہیں۔
خود کفیل Slice مثال چلائیں
ریپوزٹری میں examples/slice/ کے اندر ایک اسکرپٹ شدہ مثال شامل ہے۔ یہ صلاحیتوں کی جانچ اور تفویض کا مظاہرہ کرنے کے لیے ایک ایجنٹ، ایک ورکر اور فائل سسٹم سروس شروع کرتی ہے۔
یہ مثال کسی ماڈل فراہم کنندہ سے رابطہ نہیں کرتی اور نہ ہی اسے ماڈل اسناد یا Open Math OS کی تعیناتی درکار ہے۔ یہ انٹرایکٹو چیٹ، Ultramath، میموری یا ثبوت کی تلاش بھی شروع نہیں کرتی۔ پھر بھی Linux اور فعال bubblewrap پابندی ضروری ہے۔
مرحلہ 1: مثال شروع کریں
ریپوزٹری کی جڑ سے یہ کمانڈ چلائیں:
cargo run --locked --manifest-path cli/Cargo.toml -- run examples/slice/config.jsonمرحلہ 2: مظاہرے کو سمجھیں
چلنے کے دوران اسکرپٹ شدہ ایجنٹ تین اہم قسم کی سرگرمیاں انجام دیتا ہے:
- یہ ان فائلوں کو پڑھتا ہے جن تک رسائی کی اس کی تفویض کردہ صلاحیتیں اجازت دیتی ہیں۔
- یہ ایک چھوٹی ڈائریکٹری تک رسائی اپنے ورکر کو تفویض کرتا ہے۔
- یہ ایسی کارروائیوں کی کوشش کرتا ہے جن سے کرنل انکار کر دیتا ہے کیونکہ وہ اس کے اختیار سے تجاوز کرتی ہیں۔
اس طرح Slice مثال پروجیکٹ کے مرکزی اصول کا مختصر مظاہرہ بن جاتی ہے: کوئی پراسیس صرف وہی صلاحیتیں استعمال اور تفویض کر سکتا ہے جو حقیقتاً اس کے پاس ہوں۔
مرحلہ 3: نتائج کا معائنہ کریں
چلنے کے بعد ایجنٹ اور ورکر کے ٹرانسکرپٹس دیکھیں:
examples/slice/out/agent/transcript.jsonl
examples/slice/out/agent/worker/transcript.jsonlفائل سسٹم سروس موصول ہونے والی کالز کو الگ سے ریکارڈ کرتی ہے:
examples/slice/log/access.jsonlیہ مثال یہ رپورٹ بھی تیار کرتی ہے:
examples/slice/data/work/report.txtٹرانسکرپٹس کا فائل سسٹم ایکسیس لاگ سے موازنہ کریں تاکہ معلوم ہو سکے کہ کون سے آپریشنز کی درخواست کی گئی، کون سے تفویض کیے گئے، قبول کیے گئے یا مسترد کیے گئے۔
مثال دوبارہ چلائیں
تیار ہونے والی report.txt فائل بار بار چلانے پر اثر انداز ہوتی ہے۔ اگر آپ دوبارہ رپورٹ کامیابی سے بنانا چاہتے ہیں تو مثال دوبارہ چلانے سے پہلے اسے حذف کریں:
rm examples/slice/data/work/report.txt
cargo run --locked --manifest-path cli/Cargo.toml -- run examples/slice/config.jsonپرانے ٹرانسکرپٹ اور لاگ فائلیں برقرار رکھنا مختلف رنز کے رویے کا موازنہ کرنے میں مفید ہو سکتا ہے، اس لیے اضافی آرٹی فیکٹس حذف کرنے سے پہلے آؤٹ پٹ ڈائریکٹریز کا جائزہ لیں۔
ٹیسٹ سوٹ چلائیں
ورک اسپیس بنانے کے بعد، ریپوزٹری کی جڑ سے پہلے سے طے شدہ Rust ٹیسٹس چلائیں:
cargo test --workspaceپہلے سے طے شدہ ٹیسٹ سوٹ کے لیے ادائیگی والے ماڈل APIs یا پروڈکشن اسناد درکار نہیں ہیں۔ کچھ انٹیگریشن ٹیسٹس حقیقی چائلڈ پراسیسز شروع کرتے ہیں اور bubblewrap استعمال کرتے ہیں، اس لیے Linux کی وہی کنفائنمنٹ ضروریات لاگو ہوتی ہیں۔
ایسے ٹیسٹس جن کے لیے بیرونی ماڈل پرووائیڈرز یا Lean انسٹالیشن درکار ہو، واضح طور پر آپٹ اِن ہیں۔ ریپوزٹری کا CI ورک فلو فارمیٹنگ، Clippy، Python ٹولنگ اور Node.js MCP انٹیگریشن چیکس بھی متعین کرتا ہے۔
اعلیٰ استعمال اور ڈیولپمنٹ تجاویز
صلاحیت کی حدود کا مطالعہ کرنے کے لیے لاگز استعمال کریں
slice مثال اس وقت سب سے زیادہ مفید ہوتی ہے جب اس کی JSON Lines فائلوں کو آڈٹ ٹریل سمجھا جائے۔ ایجنٹ ٹرانسکرپٹ، ورکر ٹرانسکرپٹ اور فائل سسٹم ایکسیس لاگ کا بیک وقت جائزہ لیں۔ اس سے ظاہر ہوتا ہے کہ تفویض کردہ ایکسیس کس طرح مزید محدود ہوتا ہے اور کرنل مقررہ اختیار سے باہر کے آپریشنز کو کیسے مسترد کرتا ہے۔
تعیناتی کی ضروریات الگ رکھیں
ورک اسپیس بنانے سے خودکار طور پر مکمل مقامی Open Math OS انسٹالیشن تیار نہیں ہوتی۔ انٹرایکٹو ایجنٹس کے لیے اضافی طور پر سروس کنفیگریشن، ماڈل پرووائیڈر کی اسناد اور ایک کلائنٹ درکار ہوتا ہے۔ پروف سرچ کے لیے بھی کنفیگر شدہ Lean اور Mathlib ماحول ضروری ہے۔
deploy/vm/ میں موجود منظم VM کنفیگریشن کو عمومی مقصد کی انسٹالیشن اسکرپٹ سمجھنے سے گریز کریں۔ ریپوزٹری فی الحال slice مثال کو معاونت یافتہ خود مکمل مقامی ڈیمونسٹریشن کے طور پر دستاویز کرتی ہے۔
قابل تکرار Cargo ریزولوشن برقرار رکھیں
دستاویزی build اور run کمانڈز کے ساتھ --locked استعمال کریں۔ اس سے انحصارات کا ریزولوشن ریپوزٹری کی lockfile کے مطابق رہتا ہے اور ماحول کے درمیان غیر متوقع اختلافات کم ہوتے ہیں۔
کنفائنمنٹ کی جلد تصدیق کریں
اگر اسٹارٹ اپ ناکام ہو جائے تو اعلیٰ سطح کی سروسز کی ڈیبگنگ سے پہلے bubblewrap چیک کریں۔ تصدیق کریں کہ bwrap، PATH میں موجود ہے اور میزبان کی سیکیورٹی پالیسی غیر مراعات یافتہ user namespaces کی اجازت دیتی ہے۔ رن ٹائم مطلوبہ کنفائنمنٹ کے بغیر جان بوجھ کر جاری نہیں رہتا۔
پروف کی تصدیق کی حد سمجھیں
مکمل آرکیٹیکچر میں ایجنٹ کا اعتماد اس بات کا ثبوت نہیں ہوتا کہ کوئی تھیورم ثابت ہو چکا ہے۔ امیدوار proofs کا جائزہ محدود ورک اسپیسز میں مقررہ وقت کی حدود کے ساتھ لیا جاتا ہے، اور یہ Lean طے کرتا ہے کہ وہ کامیاب ہیں یا نہیں۔ سرچ ریکارڈز امیدوار کے کام کو محفوظ رکھتے ہیں تاکہ بعد کے راؤنڈز پہلے کی شاخوں سے جاری رہ سکیں۔
شراکت کے چیکس پر عمل کریں
تبدیلیاں تجویز کرنے سے پہلے CONTRIBUTING.md اور ریپوزٹری کے CI ورک فلو کا جائزہ لیں۔ شراکت کی رہنما دستاویز ٹیسٹنگ، AI ریویو اور پل ریکوئسٹس میں درکار معلومات بیان کرتی ہے۔
نتیجہ
Open Math Harness، Open Math OS کے لیے سیکیورٹی پر مبنی رن ٹائم کی بنیاد فراہم کرتا ہے۔ اگرچہ مکمل انٹرایکٹو ماحول ابھی تک ایک علیحدہ مقامی سیٹ اپ کے طور پر دستیاب نہیں، آپ Nucleus ورک اسپیس بنا سکتے ہیں، اس کی خود مکمل slice مثال چلا سکتے ہیں، صلاحیتوں کے نفاذ کا جائزہ لے سکتے ہیں اور پہلے سے طے شدہ ٹیسٹس چلا سکتے ہیں۔ یہ اقدامات رن ٹائم کے بنیادی اصول کا عملی تعارف فراہم کرتے ہیں: ایجنٹس واضح اختیار کے اندر تجاویز پیش کرتے اور کام کرتے ہیں، جبکہ انسان اور قابل اعتماد تصدیق کنندگان کنٹرول برقرار رکھتے ہیں۔